Zulip Chat Archive

Stream: new members

Topic: Type dependent notation

Olonbayar Temuulen (Dec 17 2023 at 10:00):

Can anyone give me a good reference to understand what it means to "The meaning of this notation is type dependent"?

Eric Wieser (Dec 17 2023 at 22:06):

Can you give some context on where you saw that sentence?

llllvvuu (Dec 17 2023 at 22:16):

I usually see that pop up when I hover over + or or something. Basically means e.g. + needs to be defined for the specific types A and B if you are trying to add a: A and b: B.

You'll need to learn about: https://lean-lang.org/theorem_proving_in_lean/type_classes.html

llllvvuu (Dec 17 2023 at 22:18):

(I think the infoview should technically know which e.g. HSMul is being used, but I don't remember how to access that)

Last updated: Dec 20 2023 at 11:08 UTC