English
The Set functor equipped with the defined Alternative structure satisfies the laws of a lawful Alternative: associativity, unit laws, and compatibility with map and orElse.
Русский
Множество как функтор, оснащённый указанной структурой Alternative, удовлетворяет законам законной Alternative: ассоциативность, законы единицы и совместимость с отображением и orElse.
LaTeX
$$$\text{Set is a LawfulAlternative}$$$
Lean4
instance : LawfulAlternative Set where
pure_seq _ _ := Set.singleton_seq
seqLeft_eq _ _ := by simp [Set.seq, Set.image2, Set.nonempty_def]
seqRight_eq s t := by simp [Set.seq, Set.image2, Set.nonempty_def]
map_pure _ _ := Set.image_singleton
seq_pure _ _ := Set.seq_singleton
seq_assoc _ _ _ := Set.seq_seq
map_failure _ := Set.image_empty _
failure_seq _ := Set.image2_empty_left
orElse_failure _ := Set.union_empty _
failure_orElse _ := Set.empty_union _
orElse_assoc _ _ _ := Set.union_assoc _ _ _ |>.symm
map_orElse _ _ _ := Set.image_union _ _ _
