source: Deliverables/D4.1/Matita/Maybe.ma @ 228

Last change on this file since 228 was 228, checked in by mulligan, 10 years ago

Conjunction, disjunction and 'xorjunction' implemented on bitvectors.
Lots of supporting datatypes. Vectors.ma includes some diabolical
dependent type hackery due to Wilmer.

File size: 761 bytes
RevLine 
[228]1include "Bool.ma".
2
3include "logic/pts.ma".
4include "Plogic/equality.ma".
5
6ninductive Maybe (A: Type[0]): Type[0] ≝
7  Nothing: Maybe A
8| Just: A → Maybe A.
9
10ndefinition is_just ≝
11  λA: Type[0].
12  λm: Maybe A.
13    match m with
14      [ Nothing ⇒ False
15      | Just j ⇒ True
16      ].
17     
18ndefinition is_nothing ≝
19  λA: Type[0].
20  λm: Maybe A.
21    match m with
22      [ Nothing ⇒ True
23      | Just j ⇒ False
24      ].
25     
26ndefinition to_maybe ≝
27  λA: Type[0].
28  λb: Bool.
29  λa: A.
30    match b with
31      [ True ⇒ Just A a
32      | False ⇒ Nothing A
33      ].
34     
35nlemma to_maybe_is_just:
36  ∀A: Type[0].
37  ∀a: A.
38  ∀b: Bool.
39    is_just A (to_maybe A b a) = b.
40  #A a b.
41  ncases b.
42  nnormalize.
43  @.
44  nnormalize.
45  @.
46nqed.
Note: See TracBrowser for help on using the repository browser.