Equations
- Flypitch.abel.LAbel = { functions := Flypitch.abel.Functions, relations := fun (x : ℕ) => PEmpty.{1} }
Instances For
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible]
Equations
- One or more equations did not get rendered due to their size.
@[reducible]
@[simp]
@[simp]
@[simp]
theorem
Flypitch.abel.realize_addTerm
(v : ℕ → intStructure.carrier)
(t₁ t₂ : fol.term LAbel)
:
fol.realize_term v (addTerm t₁ t₂) dvector.nil = fol.realize_term v t₁ dvector.nil + fol.realize_term v t₂ dvector.nil