Ignore:
Timestamp:
Nov 26, 2010, 5:38:04 PM (9 years ago)
Author:
sacerdot
Message:

REGISTER now takes a BitVector? 3

File:
1 edited

Legend:

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

    r315 r316  
    146146//; ndestruct; //.
    147147nqed.
     148
     149ndefinition head8 ≝ λA. split A (S Z) (S (S (S (S (S (S (S Z))))))).
    148150   
    149151(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    445447  @.
    446448nqed.
     449
     450naxiom eqv: ∀A,n. Vector A n → Vector A n → Bool.
Note: See TracChangeset for help on using the changeset viewer.