mathlib3 documentation

core / init.control.alternative

@[class]
structure has_orelse (f : Type u Type v) :
Type (max (u+1) v)
Instances of this typeclass
Instances of other typeclasses for has_orelse
  • has_orelse.has_sizeof_inst
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
Instances for guard
def assert {f : Type Type v} [alternative f] (p : Prop) [decidable p] :
f (inhabited p)
Equations
def optional {f : Type u Type v} [alternative f] {α : Type u} (x : f α) :
f (option α)
Equations
Instances for optional