Dot notation and coercions

Stream: new members

[Nicolò Cavalleri]

Suppose I have a linear map eval : \alpha \to\_l[R] \beta and let a : \alpha. Is there a way to use the dot notation for its evaluation (as in a.eval) but with lean still recognizing it as a linear function and hence finding the correct simp lemmas about linear functions when using simp? Reducible definition seems not to work...

[Kevin Buzzard]

Doesn't eval a just do what you want?

[Kevin Buzzard]

The way dot notation works is that a.eval means alpha.eval if a : alpha. For example if n is a natural then n.succ means nat.succ n.

[Nicolò Cavalleri]

Sorry eval was meant to be alpha.eval

[Kevin Buzzard]

Why do you want to use dot notation when eval a just works?

[Nicolò Cavalleri]

Kevin Buzzard said:

Why do you want to use dot notation when eval a just works?

Because in my case alpha is a type with a super long name and since eval is a function that it is used multiple time in algebraic expressions everything becomes unreadable

[Nicolò Cavalleri]

What should be one line becomes 5 lines

[Kevin Buzzard]

I don't really understand. How will dot notation change the length of anything when eval a is the same length as a.eval?

[Nicolò Cavalleri]

Kevin Buzzard said:

I don't really understand. How will dot notation change the length of anything when eval a is the same length as a.eval?

Well because eval is super_long_name.eval and I cant avoid protecting it because there exist multiple versions of eval for different types

[Kevin Buzzard]

If the issue is that you're writing alpha.eval a then just open alpha

[Kevin Buzzard]

Oh I see

[Kevin Buzzard]

Maybe you should just use a local abbreviation?

[Nicolò Cavalleri]

Kevin Buzzard said:

If the issue is that you're writing alpha.eval a then just open alpha

Yes I can't do that because there is acutally super_long_name_1.eval and super_long_name_2.eval

[Nicolò Cavalleri]

Kevin Buzzard said:

Maybe you should just use a local abbreviation?

And change e.g. super_long_name_1.eval to eval1 and eval2?

[Kevin Buzzard]

I'm not sure I would protect these things, if their input terms have got different types then can't Lean figure out which one you're talking about?

[Nicolò Cavalleri]

Well because one type extends the other and it is the same thing on the two types and thus it should have the same name

[Nicolò Cavalleri]

You will see in a PR before this evening I guess haha

[Nicolò Cavalleri]

For the moment I will leave the super long protected names

[Eric Wieser]

#mwe?

[Eric Wieser]

Dot notation _does_ work with simple coercions