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.
Imports
open Copy;
Table of Contents

Types

Maybe

(inductive)
inductive Maybe a
Measures
present : Bool
value : 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
{m : (Maybe a) | ! (present m)}

just

constructor
{m : (Maybe a) | present m && value m = v}

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