Leni Aniva aniva
0 Followers · 1 Following
  • Stanford University Centaur Lab
  • https://leni.sh

  • Director of NorCal Hakkero Factory No. 1

  • Joined on 2023-08-21
Repositories
12
 Projects Packages Public Activity Starred Repositories
9
aniva pushed to frontend/collect-holes at aniva/Pantograph 2024-09-09 17:38:21 -07:00
fe8b259e4f feat: Set root when there's just one mvar
aniva pushed to frontend/collect-holes at aniva/Pantograph 2024-09-09 17:35:24 -07:00
f729a357b9 Merge branch 'dev' into frontend/collect-holes
9075ded885 feat: Set `automaticMode` to true by default
Compare 2 commits »
aniva pushed to dev at aniva/Pantograph 2024-09-09 17:33:43 -07:00
9075ded885 feat: Set `automaticMode` to true by default
aniva deleted branch goal/automatic-mode from aniva/Pantograph 2024-09-09 17:33:43 -07:00
aniva merged pull request aniva/Pantograph#101 2024-09-09 17:33:42 -07:00
feat: Set `automaticMode` to true by default
aniva created pull request aniva/Pantograph#101 2024-09-09 17:30:48 -07:00
feat: Set automaticMode to true by default
aniva pushed to goal/automatic-mode at aniva/Pantograph 2024-09-09 17:30:21 -07:00
9075ded885 feat: Set `automaticMode` to true by default
aniva created branch goal/automatic-mode in aniva/Pantograph 2024-09-09 17:30:21 -07:00
aniva commented on pull request aniva/Pantograph#99 2024-09-09 17:26:02 -07:00
feat: Collect holes in Lean file and put them into a GoalState

We should probably assign the root variable when there's just one goal to avoid surprises for our users.

aniva commented on pull request aniva/Pantograph#100 2024-09-09 17:24:58 -07:00
fix: Tactics should produce .syntheticOpaque goals

Tracking https://github.com/leanprover/lean4/issues/5279

aniva pushed to frontend/collect-holes at aniva/Pantograph 2024-09-09 12:39:49 -07:00
9f0de0957e doc: Update documentation for frontend command
aniva pushed to frontend/collect-holes at aniva/Pantograph 2024-09-09 12:30:47 -07:00
762a139e78 feat: Export frontend functions
aniva pushed to frontend/collect-holes at aniva/Pantograph 2024-09-09 12:27:00 -07:00
4f5950ed78 feat: Convert holes to goals
aniva pushed to frontend/collect-holes at aniva/Pantograph 2024-09-09 10:19:40 -07:00
08fb53c020 test: Frontend process testing
aniva commented on pull request aniva/Pantograph#99 2024-09-08 15:06:40 -07:00
feat: Collect holes in Lean file and put them into a GoalState

We need to think about what the interface should look like. IMO the user should input a theorem name or line number, and the repl generates a goal state for the theorem/example/etc. on that line…

aniva pushed to frontend/collect-holes at aniva/Pantograph 2024-09-08 15:03:04 -07:00
8e3241c02a refactor: Move all frontend functions to `Frontend`
aniva created pull request aniva/Pantograph#100 2024-09-08 14:14:27 -07:00
fix: Tactics should produce .syntheticOpaque goals
aniva created branch goal/tactic in aniva/Pantograph 2024-09-08 14:14:10 -07:00
aniva pushed to goal/tactic at aniva/Pantograph 2024-09-08 14:14:10 -07:00
5e99237e09 fix: Tactics should produce `.syntheticOpaque` goals
aniva created pull request aniva/Pantograph#99 2024-09-08 13:47:30 -07:00
feat: Collect holes in Lean file and put them into a GoalState