aniva/Pantograph

v0.3.3

New issue

feat(serial): Collect auxiliary lemmas in environments and goal states
feat(goal): Branch unification (beta)
feat(goal): Overhaul infrastructure for handling conv. Introduce the fragment-based system for handling partially-executed tactics.
refactor(goal): Allow a goal state to have multiple parent goals. Delete the GoalState.focus function since it does not fit into current paradigms.

Note: There has been many modifications to the API.

2025-07-01

100% Completed

doc: Remove constraint on pick_goal

#224 by aniva was merged 2025-07-01 15:41:56 -07:00

fix(goal): Unknown metavariable problem during fragment initialization

#222 by aniva was merged 2025-06-30 15:28:29 -07:00

feat(serial): Pickle environment delta's

part/Environment

#221 by aniva was merged 2025-06-27 16:02:22 -07:00

feat(goal): Add unshielded tactic execution mode

#219 by aniva was merged 2025-06-26 15:52:17 -07:00

chore: Update version to 0.3.3

#218 by aniva was merged 2025-06-20 12:35:00 -07:00

feat(goal): Branch unification

#217 by aniva was merged 2025-06-24 13:56:15 -07:00

feat(serial): Robust environment extension pickling

part/Environment

#216 by aniva was merged 2025-06-24 13:41:06 -07:00

fix: Use the correct unfold aux lemma

#215 by aniva was merged 2025-06-20 10:21:02 -07:00

chore: Update Nix flake

#214 by aniva was merged 2025-06-20 14:03:07 -07:00

Unshielded Tactic Execution

#188 by aniva was closed 2025-06-26 15:58:34 -07:00

Branch unification

#132 by aniva was closed 2025-06-27 16:02:48 -07:00