mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
db6aa9d8d3
This PR adds a warning to any `def` of class type that does not also declare an appropriate reducibility. The warning check runs after elaboration (checking the actual reducibility status via `getReducibilityStatus`) rather than syntactically checking modifiers before elaboration. This is necessary to accommodate patterns like `@[to_additive (attr := implicit_reducible)]` in Mathlib, where the reducibility attribute is applied during `.afterCompilation` by another attribute, and would be missed by a purely syntactic check. --------- Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
68 lines
1.3 KiB
Lean4
68 lines
1.3 KiB
Lean4
module
|
||
|
||
set_option warn.classDefReducibility false
|
||
|
||
inductive Foo (α : Type u) (β : Type v) where
|
||
| mk₁ : α → Foo α β
|
||
| mk₂ : List β → Foo α β
|
||
|
||
deriving instance Nonempty for Foo
|
||
|
||
def ex1 [Nonempty α] : Nonempty (Foo α β) :=
|
||
inferInstance
|
||
|
||
inductive Bla (α : Type u) (β : Type v) where
|
||
| mk₁ : α → Bla α β
|
||
| mk₂ : β → Bla α β
|
||
|
||
deriving instance Nonempty for Bla
|
||
|
||
def ex2 [Nonempty α] : Nonempty (Bla α β) :=
|
||
inferInstance
|
||
|
||
structure Point (α : Type) where
|
||
x : α
|
||
y : α
|
||
deriving Nonempty
|
||
|
||
def ex3 [Nonempty α] : Nonempty (Point α) :=
|
||
inferInstance
|
||
|
||
inductive Lst (α : Type) where
|
||
| nil
|
||
| cons : α → Lst α → Lst α
|
||
deriving Nonempty
|
||
|
||
def ex4 : Nonempty (Lst α) :=
|
||
inferInstance
|
||
|
||
mutual
|
||
|
||
inductive FooLst (α : Type) where
|
||
| nil
|
||
| cons : Boo α → FooLst α → FooLst α
|
||
deriving Nonempty
|
||
|
||
inductive Boo (α : Type) where
|
||
| node : FooLst α → Boo α
|
||
deriving Nonempty
|
||
|
||
end
|
||
|
||
def ex5 : Nonempty (Boo α) :=
|
||
inferInstance
|
||
|
||
/-! Public structures with private fields should yield public opaque instances. -/
|
||
|
||
public structure PrivField where
|
||
private a : Nat
|
||
deriving Nonempty
|
||
|
||
/--
|
||
info: theorem instNonemptyPrivField : Nonempty PrivField :=
|
||
<not imported>
|
||
-/
|
||
#guard_msgs in
|
||
#with_exporting
|
||
#print instNonemptyPrivField
|