Changeset 857


Ignore:
Timestamp:
May 30, 2011, 4:37:25 PM (8 years ago)
Author:
sacerdot
Message:

Notations.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r856 r857  
    138138    foldl ? ? (append ?) [ ] l.
    139139
    140 (*definition if_then_else ≝
    141   λA: Type[0].
    142   λb: bool.
    143   λt: A.
    144   λf: A.
    145   match b with
    146   [ true ⇒ t
    147   | false ⇒ f
    148   ].*)
    149 
    150140let rec rev (A: Type[0]) (l: list A) on l ≝
    151141  match l with
     
    154144  ].
    155145   
    156 (*
    157 notation "hvbox('if' b 'then' t 'else' f)"
    158   non associative with precedence 83
    159   for @{ 'if_then_else $b $t $f }.
    160 *)
    161146notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
    162147 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
     148notation < "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
    164149 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).*)
    167150
    168151let rec fold_left_i_aux (A: Type[0]) (B: Type[0])
     
    210193for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }.
    211194
    212 notation < "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
     195notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
    213196 with precedence 10
    214197for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }.
Note: See TracChangeset for help on using the changeset viewer.