instLawfulAlternative_mathlib — Mathlib

English

The List type constructor with its alternative structure is LawfulAlternative.

Русский

Тип List с его альтернативной структурой образует LawfulAlternative.

LaTeX

$$$\\mathrm{LawfulAlternative}(\\mathrm List)$$

Lean4

instance : LawfulAlternative List where
  map_failure _ := List.map_nil
  failure_seq _ := List.flatMap_nil
  orElse_failure _ := List.append_nil _
  failure_orElse _ := List.nil_append _
  orElse_assoc _ _ _ := List.append_assoc _ _ _ |>.symm
  map_orElse _ _ _ := List.map_append

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