aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 15 Pull Requests 3 Packages Projects Releases Wiki Activity

feat(goal): Branch unification #217

Merged
aniva merged 8 commits from goal/branch-unification into dev 2025-06-24 13:56:15 -07:00
Conversation 2 Commits 8 Files Changed 8 +1 -1
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit cb7c4d2723 - Show all commits

2
Pantograph/Goal.lean
View File

@ -190,7 +190,7 @@ descendants of `src`, replay the differential `src' - src` in `dst`. Colliding
metavariable and lemma names will be automatically renamed to ensure there is no metavariable and lemma names will be automatically renamed to ensure there is no
collision. This implements branch unification. Unification might be impossible collision. This implements branch unification. Unification might be impossible
if conflicting assignments exist. -/ if conflicting assignments exist. -/
@[export pantograph_goal_state_replay] @[export pantograph_goal_state_replay_m]
protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM (Option GoalState) := do protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM (Option GoalState) := do
let srcNGen := src.coreState.ngen let srcNGen := src.coreState.ngen
let srcNGen' := src'.coreState.ngen let srcNGen' := src'.coreState.ngen