dk_opt.dk

#NAME dk_opt.

(; options ;)
option : cc.uT -> cc.uT.
Option : cc.uT -> Type.
[A] cc.eT (option A) --> Option A.

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

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.

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).