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

Last change on this file since 363 was 357, checked in by sacerdot, 10 years ago
  • stupid bug fixed in BitVectorTrie?
  • dependencies minimized, dead code removed
File size: 737 bytes
RevLine 
[228]1include "Bool.ma".
[260]2include "Plogic/equality.ma".
[228]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
[260]12      [ Nothing ⇒ false
13      | Just j ⇒ true
[228]14      ].
15     
16ndefinition is_nothing ≝
17  λA: Type[0].
18  λm: Maybe A.
19    match m with
[260]20      [ Nothing ⇒ true
21      | Just j ⇒ false
[228]22      ].
23     
24ndefinition to_maybe ≝
25  λA: Type[0].
26  λb: Bool.
27  λa: A.
28    match b with
[260]29      [ true ⇒ Just A a
30      | false ⇒ Nothing A
[228]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  @.
[260]44nqed.
Note: See TracBrowser for help on using the repository browser.