aniva/Pantograph

v0.3.7

New issue

feat(frontend): Remove drafting feature from frontend.process since it has been superseded by frontend.distil
feat(goal): Restore auxDeclNGen when restoring goal state
feat(repl): Implement MonadBacktrack for MainM
chore: Update Lean to v4.22.0
build: Use lean4-nix's output lean package directly to take advantage of caching

2025-09-01

100% Completed

fix(goal): Remove assigned mvars in GoalState.replay

#292 by aniva was merged 2025-08-25 21:40:28 -07:00

chore: Code cleanup

#286 by aniva was merged 2025-08-19 00:09:55 -07:00

feat(frontend): Set witness goal tag

#285 by aniva was merged 2025-08-18 10:44:20 -07:00

feat(repl): MonadBacktrack for EMainM

#283 by aniva was merged 2025-08-17 22:19:50 -07:00

build: Use lean4-nix's lean output directly

#282 by aniva was merged 2025-08-17 11:47:15 -07:00

test(goal): Move all Test.Tactic.Special tests into Test.Proofs.

#281 by aniva was merged 2025-08-16 14:07:23 -07:00

feat(goal): Restore auxDeclNGen when restoring GoalState

#279 by aniva was merged 2025-08-15 12:38:47 -07:00

feat(frontend): Remove sorry capturing capability from frontend.process

#277 by aniva was merged 2025-08-14 14:50:10 -07:00

chore: Update version

#276 by aniva was merged 2025-08-16 14:08:53 -07:00

Remove sorry extraction feature from frontend.process

#274 by aniva was closed 2025-08-14 14:50:10 -07:00