Sorry capture with instances doesn't work #241

New Issue

aniva · 2025-07-13T21:50:15-07:00

aniva commented

2025-07-13 21:50:15 -07:00

Vide https://github.com/leanprover-community/repl/issues/107

frontend.process {"file": "def test (α : Type) [s : Inhabited α] : α := @Inhabited.default α s", "readHeader": false, "inheritEnv": true, "sorrys": false, "typeErrorsAsGoals": false, "newConstants": false}
frontend.process {"file": "def test2 (α : Type) [Inhabited α] : α := by exact test α", "readHeader": false, "inheritEnv": true, "sorrys": false, "typeErrorsAsGoals": false, "newConstants": false}
frontend.process {"file": "example (α : Type) [Inhabited α] : α := sorry", "readHeader": false, "inheritEnv": true, "sorrys": true, "typeErrorsAsGoals": false, "newConstants": false}
goal.tactic {"stateId": 0, "tactic": "exact test α"}

Vide https://github.com/leanprover-community/repl/issues/107 ```jsonl frontend.process {"file": "def test (α : Type) [s : Inhabited α] : α := @Inhabited.default α s", "readHeader": false, "inheritEnv": true, "sorrys": false, "typeErrorsAsGoals": false, "newConstants": false} frontend.process {"file": "def test2 (α : Type) [Inhabited α] : α := by exact test α", "readHeader": false, "inheritEnv": true, "sorrys": false, "typeErrorsAsGoals": false, "newConstants": false} frontend.process {"file": "example (α : Type) [Inhabited α] : α := sorry", "readHeader": false, "inheritEnv": true, "sorrys": true, "typeErrorsAsGoals": false, "newConstants": false} goal.tactic {"stateId": 0, "tactic": "exact test α"} ```

aniva added this to the v0.3.5 milestone 2025-07-13 21:50:15 -07:00

aniva added the

labels 2025-07-13 21:50:15 -07:00

aniva self-assigned this 2025-07-13 21:50:15 -07:00

aniva added a new dependency 2025-07-13 22:58:07 -07:00

#242 fix(frontend): Capture local instances in `MetaTranslate`