dk_opt.dk 995 Bytes
Newer Older
1
#NAME dk_opt.
2
3

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

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

11
12
13
14
15
16
17
18
def match_option : A : cc.uT ->
                   P : (Option A -> cc.uT) ->
                   cc.eT (P (None A)) ->
                   (a : cc.eT A -> cc.eT (P (Some A a))) ->
                   o : Option A ->
                   cc.eT (P o).
[Hnone] match_option _ _ Hnone _ (None _) --> Hnone
[Hsome,a] match_option _ _ _ Hsome (Some _ a) --> Hsome a.
19

20
21
22
23
24
25
26
27
28
29
def 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).