roption α is the type of "partial values" of type α. It is similar to option α except the domain condition can be an arbitrary proposition, not necessarily decidable.

Convert an roption α with a decidable domain to an option

roption extensionality

roption eta expansion

a ∈ o means that o is defined and equal to a

roption extensionality

The none value in roption has a false domain and an empty function.

The some a value in roption has a true domain and the function returns a.

Convert an option α into an roption α

assert p f is a bind-like operation which appends an additional condition p to the domain and uses f to produce the value.

The bind operation has value g (f.get), and is defined when all the parts are defined.

The map operation for roption just maps the value and maintains the same domain.

unwrap o gets the value at o, ignoring the condition. (This function is unsound.)

pfun α β, or α →. β, is the type of partial functions from α to β. It is defined as α → roption β.

The domain of a partial function

Evaluate a partial function

Evaluate a partial function to return an option

Partial function extensionality

Turn a partial function into a function out of a subtype

Turn a total function into a partial function

The graph of a partial function is the set of pairs (x, f x) where x is in the domain of f.

The range of a partial function is the set of values f x where x is in the domain of f.

Restrict a partial function to a smaller domain.

The monad pure function, the total constant x function

The monad bind function, pointwise roption.bind

The monad map function, pointwise roption.map