Changeset 329 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Nov 29, 2010, 1:42:00 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vector.ma
r328 r329 35 35 (* Lookup. *) 36 36 (* ===================================== *) 37 38 naxiom succ_less_than_injective:39 ∀m, n: Nat.40 less_than_p (S m) (S n) → m < n.41 42 naxiom nothing_less_than_Z:43 ∀m: Nat.44 ¬(m < Z).45 37 46 38 nlet rec get_index (A: Type[0]) (n: Nat)
Note: See TracChangeset
for help on using the changeset viewer.