No deprecation warning in #check

Stream: lean4

[Thomas Zhu]

Is this expected behavior?

@[deprecated] def A := Unit
-- no warning
#check A
-- deprecation warning
#check List A
-- deprecation warning
#reduce A

[Thomas Zhu]

Similarly, (I don't know if related):

def A := Unit

def B.A := Unit
open B

-- no error
#check A
-- error: ambiguous
#check List A
-- error: ambiguous
#reduce A

[Kyle Miller]

#check ident is special, it doesn't elaborate the identifier. This is why #check ident and #check (ident) give different outputs. The second elaborates (ident) as a term, and the first provides a nicely pretty printed function signature.

[Kyle Miller]

It seems reasonable to provide a deprecation warning; it just needs to be coded for this case. Maybe make a Lean 4 issue?

[Thomas Zhu]

Ok, that makes sense. I will make an issue later

[Thomas Zhu]

Ok, that makes sense. I will make an issue later