Ignore:
Timestamp:
Nov 24, 2010, 3:40:37 PM (9 years ago)
Author:
mulligan
Message:

Removed all axioms from Arithmetic.ma and replaced them with implemented functions from other files. Implemented decidable equality on Nats.

File:
1 edited

Legend:

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

    r265 r275  
    4343    n ≤ m.
    4444
    45 ndefinition greater_than_or_equal_b
     45ndefinition greater_than_or_equal_b: ∀m, n: Nat. Bool
    4646  λm, n: Nat.
    4747    n ≤ m.
     
    190190interpretation "Nat exponential" 'exponential n m = (exponential n m).
    191191
     192nlet rec decidable_equality (m: Nat) (n: Nat) on m: Bool ≝
     193  match m with
     194    [ Z ⇒
     195      match n with
     196        [ Z ⇒ true
     197        | _ ⇒ false
     198        ]
     199    | S o ⇒
     200      match n with
     201        [ S p ⇒ decidable_equality o p
     202        | _ ⇒ false
     203        ]
     204    ].
     205
    192206(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    193207(* Greatest common divisor and least common multiple.                         *)
Note: See TracChangeset for help on using the changeset viewer.