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

Last change on this file since 228 was 228, checked in by mulligan, 9 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
Line 
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.