dk_opt.dk 1.13 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
#NAME dk_opt

(; options ;)
option : cc.uT -> cc.uT.
None : A : cc.uT -> cc.eT (option A).
Some : A : cc.uT -> cc.eT A -> cc.eT (option A).
match_option : A : cc.uT ->
               P : (cc.eT (option A) -> cc.uT) ->
               cc.eT (P (None A)) ->
               (a : cc.eT A -> cc.eT (P (Some A a))) ->
               o : cc.eT (option A) ->
               cc.eT (P o).
simple_match_option : A : cc.uT ->
                      return : cc.uT ->
                      cc.eT return ->
                      (a : cc.eT A -> cc.eT return) ->
                      o : cc.eT (option A) ->
                      cc.eT return
19
                    :=
20
21
22
23
24
25
26
27
                      A : cc.uT =>
                      return : cc.uT =>
                      match_option A (_x : cc.eT (option A) => return).

[A : cc.uT,
 P : cc.eT (option A) -> cc.uT,
 Hnone : cc.eT (P (None A)),
 Hsome : a : cc.eT A -> cc.eT (P (Some A a))]
28
    match_option A P Hnone Hsome (None _) --> Hnone
29
30
31
32
33
34

[A : cc.uT,
 P : cc.eT (option A) -> cc.uT,
 Hnone : cc.eT (P (None A)),
 Hsome : a : cc.eT A -> cc.eT (P (Some A a)),
 a : cc.eT A]
35
    match_option A P Hnone Hsome (Some _ a) --> Hsome a.