Changeset 1323


Ignore:
Timestamp:
Oct 7, 2011, 3:26:36 PM (8 years ago)
Author:
campbell
Message:

Reduce number of notations for destructive let on pairs to one.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1279 r1323  
    33include "arithmetics/nat.ma".
    44
     5include "utilities/pair.ma".
    56include "ASM/JMCoercions.ma".
    67
     
    1314notation "⊥" with precedence 90
    1415  for @{ match ? in False with [ ] }.
    15 
    16 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
    17  with precedence 10
    18 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
    19 
    20 (*
    21 notation > "hvbox('let' 〈ident x, ident y, ident z〉 ≝ t 'in' s)"
    22  with precedence 10
    23 for @{
    24   match $t with
    25   [ pair ${ident x} y' ⇒
    26     match y' with
    27     [ pair ${ident y} ${ident z} ⇒ $s ]
    28   ]
    29 }.
    30 *)
    3116
    3217definition ltb ≝
Note: See TracChangeset for help on using the changeset viewer.