Ignore:
Timestamp:
Nov 23, 2010, 2:30:10 PM (9 years ago)
Author:
sacerdot
Message:
  • Minimal changes to make it compile with the standard distribution of Matita once this directory is substituted to nlibrary
  • ambiguity reduced by lower-casing booleans
File:
1 edited

Legend:

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

    r247 r260  
    2424nlet rec less_than_or_equal_b (m: Nat) (n: Nat) on m: Bool ≝
    2525  match m with
    26     [ Z ⇒ True
     26    [ Z ⇒ true
    2727    | S o ⇒
    2828      match n with
    29         [ Z ⇒ False
     29        [ Z ⇒ false
    3030        | S p ⇒ less_than_or_equal_b o p
    3131        ]
     
    125125nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝
    126126  match n ≤ p with
    127     [ True ⇒ Z
    128     | False ⇒
     127    [ true ⇒ Z
     128    | false ⇒
    129129      match m with
    130130        [ Z ⇒ Z
     
    148148nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝
    149149  match n ≤ p with
    150     [ True ⇒ n
    151     | False ⇒
     150    [ true ⇒ n
     151    | false ⇒
    152152      match m with
    153153        [ Z ⇒ n
Note: See TracChangeset for help on using the changeset viewer.