Ignore:
Timestamp:
Nov 23, 2010, 2:30:10 PM (10 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/Arithmetic.ma

    r257 r260  
    11include "Universes.ma".
    2 include "Equality.ma".
     2include "Plogic/equality.ma".
    33include "Connectives.ma".
    44include "Nat.ma".
     
    3434  λb: Bool.
    3535    match b with
    36       [ False ⇒ Z
    37       | True ⇒ S Z
     36      [ false ⇒ Z
     37      | true ⇒ S Z
    3838      ].
    3939   
Note: See TracChangeset for help on using the changeset viewer.