dot notation on bundled homs

Stream: lean4

[Eric Rodriguez]

Has dot notation support changed in any way in Lean4? One thing that would be nice is to be able to support dot notation for ring homs, such as p.eval_ring_hom x (p : R[X]) or something like that, and as far as I know this is unsupported in Lean3. I did see the new dot notation that's like .inl x, however, which seems really cool!

[Kevin Buzzard]

eval_ring_hom is presumably no longer a thing in Lean 3 because Anne's new trick, right?

[Eric Rodriguez]

No, as far as I know it still has to exist :( what trick do you mean?

[Kevin Buzzard]

I just mean the ring_hom_class

[Eric Rodriguez]

you can't say that a specific ring_hom is an instance of ring_hom_class, you need a type as a whole