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

Last change on this file since 247 was 247, checked in by mulligan, 9 years ago

Changes to get directory to compile.

File size: 754 bytes
Line 
1include "Bool.ma".
2
3include "Universes.ma".
4include "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.