dk_opt.dk 1.15 KB
Newer Older
1
2
3
4
#NAME dk_opt

(; options ;)
option : cc.uT -> cc.uT.
5
6
7
8
9
10
Option : cc.uT -> Type.
[ A : cc.uT ] Option A --> cc.eT (option A).

None : A : cc.uT -> Option A.
Some : A : cc.uT -> cc.eT A -> Option A.

11
match_option : A : cc.uT ->
12
               P : (Option A -> cc.uT) ->
13
14
               cc.eT (P (None A)) ->
               (a : cc.eT A -> cc.eT (P (Some A a))) ->
15
               o : Option A ->
16
17
               cc.eT (P o).
[A : cc.uT,
18
 P : Option A -> cc.uT,
19
20
 Hnone : cc.eT (P (None A)),
 Hsome : a : cc.eT A -> cc.eT (P (Some A a))]
21
    match_option A P Hnone Hsome (None _) --> Hnone
22
[A : cc.uT,
23
 P : Option A -> cc.uT,
24
25
26
 Hnone : cc.eT (P (None A)),
 Hsome : a : cc.eT A -> cc.eT (P (Some A a)),
 a : cc.eT A]
27
    match_option A P Hnone Hsome (Some _ a) --> Hsome a.
28
29
30
31
32
33
34
35
36
37
38

simple_match_option : A : cc.uT ->
                      return : cc.uT ->
                      cc.eT return ->
                      (a : cc.eT A -> cc.eT return) ->
                      o : Option A ->
                      cc.eT return
                    :=
                      A : cc.uT =>
                      return : cc.uT =>
                      match_option A (_x : cc.eT (option A) => return).