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>
31 lines
1.1 KiB
Text
31 lines
1.1 KiB
Text
class Fintype (α : Type u) where
|
||
|
||
class Preorder (α : Type u) extends LT α, LE α where
|
||
lt := fun a b => a ≤ b ∧ ¬b ≤ a
|
||
|
||
structure Mappish (dIn dOut : Type u) [Fintype dIn] [Fintype dOut] where
|
||
k : Nat
|
||
|
||
variable {dIn dOut dOut₂ : Type} [Fintype dIn] [Fintype dOut] [Fintype dOut₂]
|
||
|
||
def IsGood [DecidableEq dOut] [DecidableEq dOut₂] (Λ : Mappish dIn dOut) (Λ₂ : Mappish dIn dOut₂) : Prop :=
|
||
∃ (D : Mappish dOut (dOut₂)), D.k = Λ.k + Λ₂.k
|
||
|
||
/--
|
||
error: failed to synthesize instance of type class
|
||
Fintype v
|
||
|
||
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
|
||
---
|
||
warning: Definition `MappishOrder` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
|
||
-/
|
||
#guard_msgs in
|
||
def MappishOrder [DecidableEq dIn] : Preorder
|
||
(Σ dOut : Sigma (fun t ↦ Fintype t × DecidableEq t), let fin := dOut.snd.1; Mappish dIn dOut.fst) where
|
||
le Λ₁ Λ₂ := by
|
||
let u := Λ₁.fst.fst;
|
||
let v := Λ₂.fst.fst;
|
||
let ⟨w,x⟩ := Λ₁.fst.snd;
|
||
let ⟨y,z⟩ := Λ₂.fst.snd;
|
||
clear y;
|
||
exact @IsGood dIn v u _ _ _ _ _ Λ₂.snd Λ₁.snd
|