Ignore:
Timestamp:
Nov 22, 2010, 7:25:53 PM (10 years ago)
Author:
mulligan
Message:

Work on ASM.ma file.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/List.ma

    r248 r256  
    2323
    2424notation "hvbox(hd break :: tl)"
    25   right associative with precedence 47
    26   for @{ 'Cons $hd $tl }.
    27 
    28 interpretation "List empty" 'Empty = (Empty ?).
    29 interpretation "List cons" 'Cons = (Cons ?).
    30  
     25  right associative with precedence 52
     26  for @{ 'cons $hd $tl }.
     27
    3128notation "[ list0 x sep ; ]"
    3229  non associative with precedence 90
    33   for @{ fold right @'Empty rec acc @{ 'Cons $x $acc } }.
     30  for ${fold right @'nil rec acc @{'cons $x $acc}}.
     31
     32interpretation "List empty" 'nil = (Empty ?).
     33interpretation "List cons" 'cons he tl = (Cons ? he tl).
    3434 
    3535notation "hvbox(l break !! break n)"
Note: See TracChangeset for help on using the changeset viewer.