Implementation: Evaluation Lambdas

@[reducible, inline]

abbrev Polynomial.Rfl.EvalArrow {R : Type u_1} [CommSemiring R] (p : Polynomial R) : Type u_1

A lambda representation of polynomial evaluations

Equations

• Polynomial.Rfl.EvalArrow = Polynomial.Rfl.Eval (fun (x : Polynomial R) => R → R) fun (x : Polynomial R) (F : R → R) => F

instance Polynomial.Rfl.instEvalArrowReflection {R : Type u_1} [CommSemiring R] : EvalReflection R (fun (x : Polynomial R) => R → R) fun (x : Polynomial R) (F : R → R) => F

A reflection system for Eval using the EvalArrow representation

Equations

• One or more equations did not get rendered due to their size.