Ignore:
Timestamp:
Nov 23, 2010, 5:05:46 PM (9 years ago)
Author:
mulligan
Message:

Test commit.

File:
1 edited

Legend:

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

    r261 r265  
    5757(* Add Boolean versions.                                                      *)
    5858ndefinition less_than_p ≝
    59   λm, n: Nat.
    60     m ≤ n ∧ ¬(m = n).
     59  λm: Nat.
     60  λn: Nat.
     61    less_than_or_equal_p (S m) n.
    6162   
    6263notation "hvbox(n break < m)"
Note: See TracChangeset for help on using the changeset viewer.