Ignore:
Timestamp:
Nov 29, 2010, 1:42:00 PM (9 years ago)
Author:
mulligan
Message:

Commit to restore deleted file.

File:
1 edited

Legend:

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

    r328 r329  
    3535(* Lookup.                                                                    *)
    3636(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    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).
    4537
    4638nlet rec get_index (A: Type[0]) (n: Nat)
Note: See TracChangeset for help on using the changeset viewer.