find notation

Stream: new members

[Horatiu Cheval]

Is there a command for printing the notations associated with a term, like an inverse of #print notation?

[Eric Wieser]

Create the term and use #check?

[Horatiu Cheval]

Well, for example #check function.comp only shows function.comp : (?M_2 → ?M_3) → (?M_1 → ?M_2) → ?M_1 → ?M_3

[Horatiu Cheval]

Oh, but #check function.comp _ _ shows ?M_4 ∘ ?M_5 : ?M_1 → ?M_3, you're right, thanks!

[Damiano Testa]

#check @... tends to work better. I learned this from Kevin.