# 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