Zulip Chat Archive

Stream: new members

Topic: Dot notation and coercions


Nicolò Cavalleri (May 24 2021 at 16:13):

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 (May 24 2021 at 16:15):

Doesn't eval a just do what you want?

Kevin Buzzard (May 24 2021 at 16:16):

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 (May 24 2021 at 16:17):

Sorry eval was meant to be alpha.eval

Kevin Buzzard (May 24 2021 at 16:18):

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

Nicolò Cavalleri (May 24 2021 at 16:19):

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 (May 24 2021 at 16:19):

What should be one line becomes 5 lines

Kevin Buzzard (May 24 2021 at 16:20):

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 (May 24 2021 at 16:21):

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 (May 24 2021 at 16:21):

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

Kevin Buzzard (May 24 2021 at 16:21):

Oh I see

Kevin Buzzard (May 24 2021 at 16:22):

Maybe you should just use a local abbreviation?

Nicolò Cavalleri (May 24 2021 at 16:22):

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 (May 24 2021 at 16:23):

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 (May 24 2021 at 16:23):

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 (May 24 2021 at 16:24):

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 (May 24 2021 at 16:24):

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

Nicolò Cavalleri (May 24 2021 at 16:24):

For the moment I will leave the super long protected names

Eric Wieser (May 24 2021 at 16:44):

#mwe?

Eric Wieser (May 24 2021 at 16:46):

Dot notation _does_ work with simple coercions


Last updated: Dec 20 2023 at 11:08 UTC