mathlib documentation

core.init.control.alternative

@[class]
structure has_orelse  :
(Type uType v)Type (max (u+1) v)
  • orelse : Π {α : Type ?}, f αf αf α

Instances
def failure {f : Type uType v} [alternative f] {α : Type u} :
f α

Equations
def guard {f : Type → Type v} [alternative f] (p : Prop) [decidable p] :

If the condition p is decided to be false, then fail, otherwise, return unit.

Equations
def assert {f : Type → Type v} [alternative f] (p : Prop) [decidable p] :
f (inhabited p)

Equations
def guardb {f : Type → Type v} [alternative f] :
boolf unit

Equations
def optional {f : Type uType v} [alternative f] {α : Type u} :
f αf (option α)

Equations