mathlib documentation

core.init.control.alternative

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

Instances
source
@[class]
structure alternative (f : Type u → Type v) :
Type (max (u+1) v)

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

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

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

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

Equations
source
def guardb {f : Type → Type v} [alternative f] (a : bool) :
f unit

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

Equations