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

Last change on this file since 260 was 260, checked in by sacerdot, 9 years ago
  • Minimal changes to make it compile with the standard distribution of Matita once this directory is substituted to nlibrary
  • ambiguity reduced by lower-casing booleans
File size: 762 bytes
Line 
1include "Bool.ma".
2
3include "Universes.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.