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 opened issue aniva/config#19 2024-09-23 19:38:53 -07:00
Add Kando
aniva commented on pull request aniva/config#18 2024-09-16 15:22:04 -07:00
feat: Emacs featureset update

We should remove scad mode as well. Its not used.

aniva commented on issue aniva/Pantograph#98 2024-09-09 23:57:59 -07:00
Use MLList from Batteries

Found a workaround in the frontend: If we can rely on map or foldl like structure we don't really need MLList.

aniva opened issue aniva/Pantograph#102 2024-09-09 23:49:44 -07:00
Timeout for tactics
aniva commented on pull request aniva/Pantograph#99 2024-09-09 19:32:41 -07:00
feat: Collect holes in Lean file and put them into a GoalState

https://github.com/lenianiva/PyPantograph/pull/13

Seems fine. Testing has passed.

aniva pushed to frontend/collect-holes at aniva/Pantograph 2024-09-09 18:43:54 -07:00
bec84f857b fix: repl build failure
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 deleted branch goal/automatic-mode from aniva/Pantograph 2024-09-09 17:33:43 -07:00
aniva pushed to dev at aniva/Pantograph 2024-09-09 17:33:43 -07:00
9075ded885 feat: Set `automaticMode` to true by default
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 created branch goal/automatic-mode in aniva/Pantograph 2024-09-09 17:30:21 -07:00
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 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