Ignore:
Timestamp:
Nov 11, 2010, 12:27:04 PM (10 years ago)
Author:
mulligan
Message:

BitVector? stuff from this morning: need further development of Nat
theory before I can write any interesting functions on BitVectors?.

File:
1 edited

Legend:

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

    r230 r231  
    5050interpretation "Nat multiplication" 'times n m = (multiplication n m).
    5151
     52nlet rec less_than_or_equal (n: Nat) (m: Nat) ≝
     53  match n with
     54    [ Z ⇒ True
     55    | S o ⇒
     56      match m with
     57        [ Z ⇒ False
     58        | S p ⇒ less_than_or_equal o p
     59        ]
     60    ].
     61   
     62notation "n break ≤ m"
     63  non associative with precedence 47
     64  for @{ 'less_than_or_equal $n $m }.
     65 
     66interpretation "Nat less than or equal" 'less_than_or_equal n m = (less_than_or_equal n m).
     67
    5268nlemma plus_zero:
    5369  ∀n: Nat.
Note: See TracChangeset for help on using the changeset viewer.