Polynomial eval function

Stream: mathlib4

[Shreyas Srinivas]

Why is the order of arguments for Polynomial.eval first x and then P, the polynomial?

[Shreyas Srinivas]

The signature borrowed from the docs is

def Polynomial.eval {R : Type u} [Semiring R] (x : R) (p : Polynomial R) : R

[Shreyas Srinivas]

Wouldn't

def Polynomial.eval {R : Type u} [Semiring R]  (p : Polynomial R) (x : R) : R

allow us to write p.eval x?

[Snir Broshi]

The current def also allows that, unless your R is also a polynomial

[Snir Broshi]

I believe the reason for the order is that Polynomial.eval x is a RingHom from polynomials, but I don't remember where that RingHom is defined

[Snir Broshi]

docs#Polynomial.evalRingHom

[Shreyas Srinivas]

Oh that's interesting. That seems unlike the usual requirement for getting the dot notation

[Snir Broshi]

Dot notation uses the first parameter of that type, it doesn't have to be the first parameter overall

[Snir Broshi]

Otherwise the R : Type* would beat it

[Shreyas Srinivas]

Thanks. TIL

[Edward van de Meent]

Shreyas Srinivas said:

Wouldn't

def Polynomial.eval {R : Type u} [Semiring R]  (p : Polynomial R) (x : R) : R

allow us to write p.eval x?

Doesn't it still do so now?

[Shreyas Srinivas]

It does. This thread can be closed. I learnt something new