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

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r856 r857 138 138 foldl ? ? (append ?) [ ] l. 139 139 140 (*definition if_then_else ≝141 λA: Type[0].142 λb: bool.143 λt: A.144 λf: A.145 match b with146 [ true ⇒ t147  false ⇒ f148 ].*)149 150 140 let rec rev (A: Type[0]) (l: list A) on l ≝ 151 141 match l with … … 154 144 ]. 155 145 156 (*157 notation "hvbox('if' b 'then' t 'else' f)"158 non associative with precedence 83159 for @{ 'if_then_else $b $t $f }.160 *)161 146 notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 162 147 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 19148 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 164 149 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).*)167 150 168 151 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 ] ] }. 211 194 212 notation < "hvbox('let' 〈ident x,ident y〉 ≝ t 'in's)"195 notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉\nbsp ≝ break t \nbsp 'in' \nbsp) break s)" 213 196 with precedence 10 214 197 for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }.
Note: See TracChangeset
for help on using the changeset viewer.