projection notation for coe_to_fun

Stream: general

[Eric Wieser]

Would it be a bad idea to hide coe_fn from the pretty-print output and use projection notation? As an example,

import data.equiv.mul_add

structure my_proj := (x : ℕ)
instance : add_monoid (my_proj) := sorry

def x : my_proj := 0

namespace my_proj

def a : my_proj → my_proj := sorry
def b : my_proj ≃ my_proj := sorry
def a' : my_proj →+ my_proj := sorry
def b' : my_proj ≃+ my_proj := sorry

end my_proj

#check x.a   -- x.a : my_proj
#check x.b   -- ⇑my_proj.b x : my_proj
#check x.a'  -- ⇑my_proj.c x : my_proj
#check x.b'  -- ⇑my_proj.d x : my_proj

If so, which of these seems like the better approach?

• Add @[pp_dot] as a dual of @[pp_nodot], and apply it to the bundled homs where it makes things clearer
• Adjust pretty_fn<T>::is_field_notation_candidate to allow projections of the form ⇑constant_name f to be printed f.constant_name

[Gabriel Ebner]

(deleted)

[Gabriel Ebner]

Maybe 0 isn't the best example to illustrate this with. How about def x : my_proj := 0 first?

[Eric Wieser]

The motivation here is some change @Anne Baanen is making to linear_map.to_bilin, which makes it an equiv and not a normal function (or perhaps not that exactly, but something equivalent)

[Gabriel Ebner]

Seems like a good idea to me. I didn't even realize that x.b worked in the first place.

[Eric Wieser]

I didn't realize it did either until I tried this out

[Eric Wieser]

I'm guessing right now we bail out on if (!is_constant(f)) return false;, and would need to change that to use is_coercion_fn somehow first

[Yury G. Kudryashov]

It works off there are no more arguments.

[Eric Wieser]

*iff?

[Yury G. Kudryashov]

Otherwise it starts looking for an argument of type ... and fails.

[Yury G. Kudryashov]

BTW, is it hard to make it work with more arguments? It works be nice to make polynomial.eval a bundled homomorphism without loosing dot notation.

[Eric Wieser]

Can you give a #mwe of a case where projection notation doesn't work?

[Yury G. Kudryashov]

docs#fin.cast_le

[Eric Wieser]

Yep, that fails with "invalid field notation, function 'fin.cast_le' does not have explicit argument with type (fin ...)"

import data.fin
variables (n : fin 2)
#check n.cast_le (le_refl _)

[Eric Wieser]

(deleted)