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/Maybe.ma

    r247 r260  
    22
    33include "Universes.ma".
    4 include "Equality.ma".
     4include "Plogic/equality.ma".
    55
    66ninductive Maybe (A: Type[0]): Type[0] ≝
     
    1212  λm: Maybe A.
    1313    match m with
    14       [ Nothing ⇒ False
    15       | Just j ⇒ True
     14      [ Nothing ⇒ false
     15      | Just j ⇒ true
    1616      ].
    1717     
     
    2020  λm: Maybe A.
    2121    match m with
    22       [ Nothing ⇒ True
    23       | Just j ⇒ False
     22      [ Nothing ⇒ true
     23      | Just j ⇒ false
    2424      ].
    2525     
     
    2929  λa: A.
    3030    match b with
    31       [ True ⇒ Just A a
    32       | False ⇒ Nothing A
     31      [ true ⇒ Just A a
     32      | false ⇒ Nothing A
    3333      ].
    3434     
Note: See TracChangeset for help on using the changeset viewer.