deprecated.lean:5:2-5:14: warning: `[deprecated]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")`
deprecated.lean:8:2-8:12: warning: `[deprecated]` attribute should specify either a new name or a deprecation message
deprecated.lean:8:2-8:12: warning: `[deprecated]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")`
deprecated.lean:11:6-11:7: warning: `f` has been deprecated: Use `g` instead
2
deprecated.lean:13:6-13:7: warning: `h` has been deprecated
1
deprecated.lean:15:13-15:15: error(lean.unknownIdentifier): Unknown constant `g1`
deprecated.lean:23:13-23:15: error(lean.unknownIdentifier): Unknown constant `g1`
deprecated.lean:27:2-27:55: warning: `[deprecated]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")`
deprecated.lean:30:6-30:8: warning: `f2` has been deprecated: Use `Foo.g1` instead

Note: The updated constant has a different type:
  Nat
instead of
  Nat → Nat
2
2
deprecated.lean:33:6-33:8: warning: `f4` has been deprecated: use g1 instead, f4 is not a good name
2
deprecated.lean:35:2-35:12: warning: `[deprecated]` attribute should specify either a new name or a deprecation message
deprecated.lean:35:2-35:12: warning: `[deprecated]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")`