fix(goal): Unknown metavariable problem during fragment initialization #222

aniva · 2025-06-30T14:43:30-07:00

aniva commented

2025-06-30 14:43:30 -07:00

To reproduce:

options.set {"automaticMode": false}
goal.start {"expr": "∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b"}
goal.tactic {"stateId": 0, "tactic": "intro a b h"}
goal.tactic {"stateId": 1, "mode": "calc"}
goal.tactic {"stateId": 2, "tactic": "1 + a + 1 = a + 1 + 1"}
goal.tactic {"stateId": 3, "mode": "conv"}

To reproduce: ```jsonl options.set {"automaticMode": false} goal.start {"expr": "∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b"} goal.tactic {"stateId": 0, "tactic": "intro a b h"} goal.tactic {"stateId": 1, "mode": "calc"} goal.tactic {"stateId": 2, "tactic": "1 + a + 1 = a + 1 + 1"} goal.tactic {"stateId": 3, "mode": "conv"} ```

aniva added this to the 0.3.3 milestone 2025-06-30 14:43:30 -07:00

aniva added the

category

feature

part/Goal

labels 2025-06-30 14:43:30 -07:00

aniva self-assigned this 2025-06-30 14:43:30 -07:00

aniva added 1 commit 2025-06-30 14:53:04 -07:00

8857b88d9a

fix(goal): Restore elaboration monad

aniva added 1 commit 2025-06-30 15:00:42 -07:00

dd7c6c36c8