3.6 Maybe

8.12

package: cur-lib

This library defines the datatype Maybe and several forms for using them.

1 parameter type
Maybe : (-> (A : Type) Type)
constructor
none : (-> (A : Type) (Maybe A))
constructor
some : (-> (A : Type) (a : A) (Maybe A))

The maybe datatype.

syntax
(some/i a)

A syntactic form for some that attempts to infer the type of the expression a to reduce annotation burden.

Examples:

> (some Bool true)
(some (Bool) (true))
> (some/i true)
some/i: unbound identifier in module