Topic: algebra classes
Kenny Lau (May 10 2020 at 05:41):
What are the uses of algebra classes such as the following?
@[algebra] class is_symm_op (α : Type u) (β : out_param (Type v)) (op : α → α → β) : Prop := (symm_op : ∀ a b, op a b = op b a) @[algebra] class is_left_distrib (α : Type u) (op₁ : α → α → α) (op₂ : out_param $ α → α → α) : Prop := (left_distrib : ∀ a b c, op₁ a (op₂ b c) = op₂ (op₁ a b) (op₁ a c))
Last updated: May 15 2021 at 00:39 UTC