Changeset 856 for src/ASM/Util.ma
 Timestamp:
 May 30, 2011, 1:44:45 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r782 r856 138 138 foldl ? ? (append ?) [ ] l. 139 139 140 definition if_then_else ≝140 (*definition if_then_else ≝ 141 141 λA: Type[0]. 142 142 λb: bool. … … 146 146 [ true ⇒ t 147 147  false ⇒ f 148 ]. 148 ].*) 149 149 150 150 let rec rev (A: Type[0]) (l: list A) on l ≝ … … 159 159 for @{ 'if_then_else $b $t $f }. 160 160 *) 161 notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. 162 notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. 163 164 interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f). 161 notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 162 for @{ match $e in bool with [ true ⇒ $t  false ⇒ $f] }. 163 notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 164 for @{ match $e with [ true ⇒ $t  false ⇒ $f] }. 165 166 (*interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f).*) 165 167 166 168 let rec fold_left_i_aux (A: Type[0]) (B: Type[0]) … … 207 209 with precedence 10 208 210 for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }. 211 212 notation < "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" 213 with precedence 10 214 for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }. 209 215 210 216 notation "⊥" with precedence 90
Note: See TracChangeset
for help on using the changeset viewer.