Commit Graph

17 Commits

Author SHA1 Message Date
Leni Aniva ea813e5bc5
feat: Monadic info collection 2024-12-08 23:21:36 -08:00
Leni Aniva c54ce93ef5
feat: Goal State IO in REPL 2024-12-05 14:31:43 -08:00
Leni Aniva 0f946880ae
test: Environment pickling 2024-12-04 10:44:33 -08:00
Leni Aniva 2790553180
feat: Environment save/load commands 2024-11-13 19:50:31 -08:00
Leni Aniva ee8063e1f5
refactor: Merge all Delation functions 2024-11-08 14:41:24 -08:00
Leni Aniva 72e41e1e1e
Merge branch 'dev' into frontend/environment 2024-10-12 16:57:55 -07:00
Leni Aniva 5a2ae880f4
feat: Capture environment in drafting 2024-10-12 16:46:44 -07:00
Leni Aniva 645d9c9250
feat: Let tactic in REPL 2024-10-12 16:17:21 -07:00
Leni Aniva c3076cbb7d
chore: Update Lean to v4.12.0 2024-10-06 16:10:18 -07:00
Leni Aniva d0321e72dd
feat: Add message diagnostics to frontend.process 2024-10-05 14:49:17 -07:00
Leni Aniva 4f5950ed78
feat: Convert holes to goals 2024-09-09 12:26:46 -07:00
Leni Aniva 08fb53c020
test: Frontend process testing 2024-09-09 10:18:20 -07:00
Leni Aniva 8e3241c02a
refactor: Move all frontend functions to `Frontend` 2024-09-08 15:02:43 -07:00
Leni Aniva b645d79fda
Merge branch 'dev' into goal/automatic 2024-09-08 12:13:42 -07:00
Leni Aniva e4d53733d0
feat: Simplify repl 2024-09-07 14:03:29 -07:00
Leni Aniva 9b3eef35ec
fix: Forgot to include the current goals in resume 2024-09-06 22:22:19 -07:00
Leni Aniva a7b30af36b
refactor: Refactor REPL out of main library
fix: Calc previous rhs not found bug
2024-09-06 22:01:36 -07:00