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

Work on ASM.ma file.

File:
1 edited

Legend:

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

    r248 r256  
    2626(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    2727
    28 notation "hvbox(hd break :: tl)"
    29   right associative with precedence 52
    30   for @{ 'Cons $hd $tl }.
    31  
    32 interpretation "Vector cons" 'Cons hd tl = (Cons ? ? hd tl).
     28interpretation "Vector nil" 'nil = (Empty ?).
     29interpretation "Vector cons" 'cons hd tl = (Cons ? ? hd tl).
    3330
    3431notation "hvbox (v break !! n)"
Note: See TracChangeset for help on using the changeset viewer.