lean4/tests/elab/structFieldAttrs.lean at 33725c584e3dbe675fe7aa8370c4fbe317f1f151 · leanprover/lean4 · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
-- Tests for attributes on structure fields.
-- Attributes on fields are applied to the generated projection functions.

import Lean

/-! ### @[deprecated] on a field -/

structure Foo where
  @[deprecated "Use y instead!" (since := "2025-04-30")] x : Nat
  y : Bool

/-! ### @[inline] on a field -/

structure Baz where
  @[inline] compute : Nat → Nat

/-! ### @[reducible] on a class field (class projections are semireducible by default) -/

class MyClass (α : Type) where
  @[reducible] default : α

/-! ### Field with default -/

structure WithDefault where
  @[deprecated "Stop!" (since := "2025-04-30")] x : Nat := 42

/-! ### Verify attributes were applied to projections -/

/-- info: true -/
#guard_msgs in
#eval do return Lean.Linter.isDeprecated (← Lean.getEnv) ``Foo.x

/-- info: true -/
#guard_msgs in
#eval do return Lean.Linter.isDeprecated (← Lean.getEnv) ``WithDefault.x