On this page:
Maybe
none
some
some/  i
7.1

3.6 Maybe

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 (Bool) (true))