Changeset 857 for src

Timestamp:

May 30, 2011, 4:37:25 PM (10 years ago)

Author:

sacerdot

Message:

Notations.

File:

• src/ASM/Util.ma (modified) (3 diffs)

src/ASM/Util.ma

@@ -138 +138 @@
     foldl ? ? (append ?) [ ] l.
 
-(*definition if_then_else ≝
-  λA: Type[0].
-  λb: bool.
-  λt: A.
-  λf: A.
-  match b with
-  [ true ⇒ t
-  | false ⇒ f
-  ].*)
-
 let rec rev (A: Type[0]) (l: list A) on l ≝ 
   match l with
@@ -154 +144 @@
   ]. 
     
-(*
-notation "hvbox('if' b 'then' t 'else' f)"
-  non associative with precedence 83
-  for @{ 'if_then_else $b $t $f }.
-*)
 notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
  for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f]  }.
-notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19
+notation < "hvbox('if' \nbsp term 19 e \nbsp break 'then' \nbsp term 19 t \nbsp break 'else' \nbsp term 48 f \nbsp" non associative with precedence 19
  for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }.
-
-(*interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f).*)
 
 let rec fold_left_i_aux (A: Type[0]) (B: Type[0])
@@ -210 +193 @@
 for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }.
 
-notation < "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
+notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
  with precedence 10
 for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }.