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

Last change on this file since 419 was 357, checked in by sacerdot, 10 years ago
  • stupid bug fixed in BitVectorTrie?
  • dependencies minimized, dead code removed
File size: 737 bytes
Line 
1include "Bool.ma".
2include "Plogic/equality.ma".
3
4ninductive Maybe (A: Type[0]): Type[0] ≝
5  Nothing: Maybe A
6| Just: A → Maybe A.
7
8ndefinition is_just ≝
9  λA: Type[0].
10  λm: Maybe A.
11    match m with
12      [ Nothing ⇒ false
13      | Just j ⇒ true
14      ].
15     
16ndefinition is_nothing ≝
17  λA: Type[0].
18  λm: Maybe A.
19    match m with
20      [ Nothing ⇒ true
21      | Just j ⇒ false
22      ].
23     
24ndefinition to_maybe ≝
25  λA: Type[0].
26  λb: Bool.
27  λa: A.
28    match b with
29      [ true ⇒ Just A a
30      | false ⇒ Nothing A
31      ].
32     
33nlemma to_maybe_is_just:
34  ∀A: Type[0].
35  ∀a: A.
36  ∀b: Bool.
37    is_just A (to_maybe A b a) = b.
38  #A a b.
39  ncases b.
40  nnormalize.
41  @.
42  nnormalize.
43  @.
44nqed.
Note: See TracBrowser for help on using the repository browser.