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

13

Projects Packages Public Activity Starred Repositories

9

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

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 pushed to goal/tactic at aniva/Pantograph 2024-09-08 14:14:10 -07:00

5e99237e09 fix: Tactics should produce `.syntheticOpaque` goals

aniva created branch goal/tactic in aniva/Pantograph 2024-09-08 14:14:10 -07:00

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

aniva created branch frontend/collect-holes in aniva/Pantograph 2024-09-08 13:45:21 -07:00

aniva pushed to frontend/collect-holes at aniva/Pantograph 2024-09-08 13:45:21 -07:00

860344f9c5 refactor: Factor out `FrontendM` driver

aniva closed issue aniva/Pantograph#93 2024-09-08 13:40:12 -07:00

Refactor out the Pantograph executable and lib into different targets

aniva commented on issue aniva/Pantograph#93 2024-09-08 13:40:12 -07:00

Refactor out the Pantograph executable and lib into different targets

Done #92

aniva opened issue aniva/Pantograph#98 2024-09-08 13:39:37 -07:00

Use MLList from Batteries