- value : α
- neutral : Option (PLift (Std.LawfulIdentity op self.value))
Instances For
- op : α → α → α
- assoc : Std.Associative self.op
- comm : Option (PLift (Std.Commutative self.op))
- idem : Option (PLift (Std.IdempotentOp self.op))
- arbitrary : α
Instances For
Equations
Equations
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
theorem
Lean.Data.AC.Context.unwrap_isNeutral
{α : Sort u_1}
{ctx : Context α}
{x : Nat}
:
ContextInformation.isNeutral ctx x = true →
Std.LawfulIdentity (EvalInformation.evalOp ctx) (EvalInformation.evalVar ctx x)
theorem
Lean.Data.AC.Context.evalList_removeNeutrals
{α : Sort u_1}
(ctx : Context α)
(e : List Nat)
: