instAlternative — Mathlib

English

The Filter type carries an Alternative structure with seq defined by x.seq(y()) and failure bottom, orElse by x ⊔ y().

Русский

У типа Filter имеется структура Alternative: последовательность определяется как x.seq(y()), нулевая часть — ⊥, операция выбора — x ⊔ y().

LaTeX

$$$ \text{Alternative}(\text{Filter}) \text{ with } \text{seq}(x,y)=x.seq(y()),\ \text{failure}=\bot,\ \text{orElse}(x,y)=x \sqcup y $.$$

Lean4

instance : Alternative Filter where
  seq := fun x y => x.seq (y ())
  failure := ⊥
  orElse x y := x ⊔ y ()

Похожие утверждения