Changeset 1161 for src/ASM/Util.ma


Ignore:
Timestamp:
Aug 31, 2011, 6:24:03 PM (8 years ago)
Author:
mulligan
Message:

changes from today: merged ertl, ltl and lin into one datatype to simplify semantics

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1159 r1161  
    1717 with precedence 10
    1818for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
     19
     20(*
     21notation > "hvbox('let' 〈ident x, ident y, ident z〉 ≝ t 'in' s)"
     22 with precedence 10
     23for @{
     24  match $t with
     25  [ pair ${ident x} y' ⇒
     26    match y' with
     27    [ pair ${ident y} ${ident z} ⇒ $s ]
     28  ]
     29}.
     30*)
    1931
    2032definition ltb ≝
Note: See TracChangeset for help on using the changeset viewer.