maybe

Maybe package contains inductive data type definition representing value container with optional empty constructor.

data maybe (A: U) = nothing | just (a: A)

nothing

nothing is basic maybe point constructor.

null: maybe nat = nothing

just

just is maybe value wrapper.

wrapped: maybe nat = just one

Generics

maybe (A B: U) (n: B) (j: A -> B) : maybe A -> B

Returns a function from wrapped to raw values.

> maybe_ nat nat zero (\ (x: nat) -> x) (just zero)
EVAL: zero