Changeset 856 for src/ASM/Util.ma


Ignore:
Timestamp:
May 30, 2011, 1:44:45 PM (9 years ago)
Author:
sacerdot
Message:
  1. if_then_else is now a notation for match with (to allow Russell to work better)
  2. notation for destructuring let fixed to work in pretty printing mode too
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r782 r856  
    138138    foldl ? ? (append ?) [ ] l.
    139139
    140 definition if_then_else ≝
     140(*definition if_then_else ≝
    141141  λA: Type[0].
    142142  λb: bool.
     
    146146  [ true ⇒ t
    147147  | false ⇒ f
    148   ].
     148  ].*)
    149149
    150150let rec rev (A: Type[0]) (l: list A) on l ≝
     
    159159  for @{ 'if_then_else $b $t $f }.
    160160*)
    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).
     161notation > "'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]  }.
     163notation < "'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).*)
    165167
    166168let rec fold_left_i_aux (A: Type[0]) (B: Type[0])
     
    207209 with precedence 10
    208210for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }.
     211
     212notation < "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
     213 with precedence 10
     214for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }.
    209215
    210216notation "⊥" with precedence 90
Note: See TracChangeset for help on using the changeset viewer.