db491ddd35
This PR moves the issue tracking infrastructure from `GrindM` to `SymM`. Issues can occur in different places within a `sym =>` block (e.g., during arithmetic normalization, simplification), not just during `grind` invocations. Moving them to `SymM` makes them available to all modules operating within the symbolic computation framework. - `Sym.reportIssue`: adds an issue to the `SymM` state - `Sym.getIssues`: retrieves accumulated issues - `Sym.withNewIssueContext`: saves/restores the issue list around a computation, used at grind entry points to isolate per-invocation issues while preserving them in the outer context - `GrindM.State.issues` removed; `Grind.reportIssue` delegates to `Sym.reportIssue` 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
24 lines
740 B
Text
24 lines
740 B
Text
module
|
|
structure Cat (C : Type) where
|
|
hom : C → C → Type
|
|
comp {x y z : C} (f : hom x y) (g : hom y z) : hom x z
|
|
id x : hom x x
|
|
|
|
structure Foo {C D : Type} (ℭ₁ : Cat C) (ℭ₂ : Cat D) where
|
|
obj : C → D
|
|
|
|
variable {C D : Type} {ℭ₁ : Cat C} {ℭ₂ : Cat D}
|
|
|
|
structure Iso (x y : C) where
|
|
hom : ℭ₁.hom x y
|
|
inv : ℭ₁.hom y x
|
|
hom_inv_id : ℭ₁.comp hom inv = ℭ₁.id _
|
|
inv_hom_id : ℭ₁.comp hom inv = ℭ₁.id _
|
|
|
|
attribute [grind =] Iso.hom_inv_id Iso.inv_hom_id
|
|
|
|
#guard_msgs in -- Should not produce any issues
|
|
set_option trace.sym.issues true in
|
|
example (F G : Foo ℭ₁ ℭ₂) (e : ∀ (x : C), Iso (F.obj x) (G.obj x)) (x : C) :
|
|
ℭ₂.comp (e x).hom (e x).inv = ℭ₂.id _ := by
|
|
grind
|