deprecation and arguments

Stream: lean4

[Damiano Testa]

I was surprised to only get a deprecation warning when an argument is passed to the lemma:

@[deprecated]
theorem depr (_ : Unit) : True := .intro

@[deprecated]
theorem depr_no_arg : True := .intro

-- no deprecation
#check depr
#check depr_no_arg

-- `depr` has been deprecated
#check depr ()

Is this expected behaviour?

[Sebastian Ullrich]

This is likely specific to #check? It shouldn't happen in actual code

[Damiano Testa]

Probably yes: I have not observed this happening in actual code.

[Damiano Testa]

I tried a bit and #check and #print do not trigger a deprecation, but more or less everything else that I tried worked as expected. I found the closely related examples below amusing, though I probably understand why this is the expected behaviour:

@[deprecated]
theorem depr (_ : Unit) : True := .intro

@[deprecated]
theorem depr_no_arg : True := .intro

variable (a : True := by exact depr_no_arg) in
example : True := a     -- no deprecations

variable (a : True := by exact depr ()) in
example : True := a     -- no deprecations

variable (a : Unit → True := by exact depr) in
example : True := a ()  -- no deprecations

structure A where
  a : True := by exact depr ()
  b : True := by exact depr_no_arg
  c : Unit → True := by exact depr

-- 3 deprecations
example : A := {}

In all cases, removing by exact does trigger a deprecation.