Ignore:
Timestamp:
Nov 22, 2010, 11:43:04 AM (9 years ago)
Author:
mulligan
Message:

More changes. Added datatype for addressing modes.

File:
1 edited

Legend:

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

    r246 r248  
    1111include "List.ma".
    1212include "Cartesian.ma".
    13 
     13include "Maybe.ma".
    1414include "Equality.ma".
    1515
     
    221221    | Cons o hd tl ⇒ ? (append A o ? (reverse A o tl) (Cons A Z hd (Empty A)))
    222222    ].
     223    nrewrite < (succ_plus ? ?).
     224    nrewrite > (plus_zero ?).
    223225    //.
    224226nqed.
     
    262264          ]
    263265    ].
     266    nrewrite < (succ_plus ? ?).
     267    nrewrite > (plus_zero ?).
    264268    //.
    265269nqed.
Note: See TracChangeset for help on using the changeset viewer.