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

(; options ;)
4
5
def option := cc.option.
def Option := cc.Option.
6
7
8
9

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

10
11
12
13
14
15
16
17
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.
18

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