Lean4でdot表記のときdeprecatedが有効化されない
code:depl.lean
@deprecated theorem Nat.deprfl (n : Nat) : n = n := rfl -- expected: deprecation warning
example {n : Nat} : n = n := Nat.deprfl n
-- unexpected: no deprecation warning
example {n : Nat} : n = n := n.deprfl
このときn.deprflのほうが警告が出ない.