Maybe

A value that is either present (``just v``) or absent (``none``). Models Python's ``None`` sentinel, partial functions, and any operation that may not produce a result. ``Maybe a`` is a polymorphic inductive type so the same library serves ``Maybe Int``, ``Maybe String``, etc.
Table of Contents

Types

Maybe

(inductive)
inductive Maybe a

Constructors

For each type in this module: inductive types list their declared constructors; opaque types list any local function whose name starts with mk and which returns a value of that type.

Maybe (inductive)

none

constructor
Maybe a

just

constructor
Maybe a

Functions

isNone

Returns ``true`` when the value is absent.
def isNone (m: Maybe a) : Bool

isJust

Returns ``true`` when the value is present.
def isJust (m: Maybe a) : Bool

withDefault

Returns the contained value, or ``d`` if the value is absent.
def withDefault (d: a) (m: Maybe a) : a