Commit Graph

358 Commits

Author SHA1 Message Date
Leni Aniva ef864ea16d feat(lib): Option creation function 2024-03-10 15:33:32 -07:00
Leni Aniva 0b91c41ad2 fix: Execute expr parsing within goal.start 2024-03-10 15:09:38 -07:00
Leni Aniva a5b0721482 feat(lib): Expose goal state interface 2024-03-10 08:13:10 -07:00
Leni Aniva 996f16bbb8 feat(lib): CoreM execution function 2024-03-10 06:41:35 -07:00
Leni Aniva f18a9dd1d5 refactor: Move some functions to `Library.lean` 2024-03-09 20:37:48 -08:00
Leni Aniva eeb149a32c feat(lib): Search path function 2024-03-09 19:36:25 -08:00
Leni Aniva 2ad7ad8778 feat(lib): Catalog command FFI 2024-03-09 16:50:36 -08:00
Leni Aniva 7bc0f82654 feat: Add exported version function 2024-03-08 23:50:44 -08:00
Leni Aniva 267d635c05 feat(build): Add shared facet for lean_lib 2024-03-06 15:27:22 -08:00
Leni Aniva 93b7d8b67d feat: Output shared library in flake 2024-03-06 15:26:35 -08:00
Leni Aniva 7e28ded23f test: More diagnostics for tests 2024-03-06 15:14:08 -08:00
Leni Aniva cb0712ccf6 Merge pull request 'feat: Print parent expression assignment' (#45) from goal/relation into dev
Reviewed-on: #45
2024-02-15 14:55:02 -08:00
Leni Aniva 111781816f test: Delayed metavariable assignment 2024-02-15 14:47:09 -08:00
Leni Aniva 18c318cb73 Merge branch 'dev' into goal/relation 2024-02-15 14:39:30 -08:00
Leni Aniva 0254759581 Merge pull request 'feat: Add leanpkgs to the flake output' (#46) from nix/toolchain into dev
Reviewed-on: #46
2024-02-15 14:30:30 -08:00
Leni Aniva df4e044e5f chore: Expose `leanPkgs` in flake 2024-02-13 15:30:56 -05:00
Leni Aniva 5f5d06f1d8 feat: Add lake and lean to the package output 2024-02-05 11:50:22 -08:00
Leni Aniva 4acd367ca7 chore: Version bump to 0.2.12-alpha 2024-01-30 17:45:32 -08:00
Leni Aniva fe5c1eda7d feat: Prevent crash during rootExpr call 2024-01-30 17:22:20 -08:00
Leni Aniva 40d61fecc5 doc: Correct comment about parent filling expr 2024-01-30 16:37:35 -08:00
Leni Aniva 25f3a2f19d feat: Print parent expression assignment 2024-01-24 18:19:04 -08:00
Leni Aniva d5ef05a7b0 Merge pull request 'test: Option controlled mvar instantiation' (#44) from goal/diag into dev
Reviewed-on: #44
2024-01-17 22:27:44 -08:00
Leni Aniva 34d9b02797 Merge branch 'dev' into goal/diag 2024-01-17 14:03:19 -08:00
Leni Aniva 30eda7ef8c Merge pull request 'feat: Print inductives, constructors, and recursors in env.inspect' (#43) from env/inspect into dev
Reviewed-on: #43
2024-01-17 14:02:55 -08:00
Leni Aniva 6a81d83c1f test: Option controlled mvar instantiation 2024-01-16 16:44:54 -08:00
Leni Aniva 50ac2fea4b feat: Print constructor and recursor info 2024-01-16 14:11:52 -08:00
Leni Aniva 6fb1b2e787 feat: Print inductives in env.inspect 2024-01-16 13:29:30 -08:00
Leni Aniva 6692303da6 test: Simplify monad execution 2024-01-07 14:14:20 -08:00
Leni Aniva a8bfa56587 Merge pull request 'feat: Add definitions and theorems to the environment' (#41) from env/add-decl into dev
Reviewed-on: #41
2023-12-26 12:41:01 -08:00
Leni Aniva 1c370ef2ae refactor: Rename Test/{Catalog,Environment} 2023-12-26 12:22:57 -05:00
Leni Aniva dc90b6b73e chore: Move environment functions to its own file
Symbol.lean is now subsumed
2023-12-15 13:40:36 -05:00
Leni Aniva da194a1165 refactor: env. operations into its own file 2023-12-15 13:37:55 -05:00
Leni Aniva aef93cf506 fix: Force instantiate all mvars in env.add 2023-12-15 13:07:59 -05:00
Leni Aniva a540dd4540 test: env.add 2023-12-14 11:11:24 -08:00
Leni Aniva 85eb42207c fix: env_add monads 2023-12-14 05:52:12 -08:00
Leni Aniva 69be7c3920 Merge branch 'dev' into env/add-decl 2023-12-14 05:48:49 -08:00
Leni Aniva 83ff58dffc Merge pull request 'feat: Change the main interaction monad' (#40) from core/loop into dev
Reviewed-on: #40
2023-12-14 05:46:39 -08:00
Leni Aniva 3c96a7c0ea feat: env_add command 2023-12-13 19:35:32 -08:00
Leni Aniva ff4671cdd0 chore: Rename lib. commands to env.
This is done to improve clarity and align with Lean's terminology
2023-12-12 18:56:25 -08:00
Leni Aniva 085b12c255 feat: Use CoreM as the main interaction monad 2023-12-12 18:39:02 -08:00
Leni Aniva ac9f6f810c doc: TermElabM metavariable generation 2023-12-08 17:32:30 -08:00
Leni Aniva bd0c66facc fix: Consolidate TermElabM blocks 2023-12-08 17:31:25 -08:00
Leni Aniva 2fe4fa9bc4 fix: Change the main interaction monad to MetaM 2023-12-08 16:17:16 -08:00
Leni Aniva d7fcc502f9 chore: Version downgrade to 0.2.10-alpha
There is a currently known bug
2023-12-07 12:38:02 -08:00
Leni Aniva 94c4b2cfe3 Merge pull request 'fix: Printing projection leads to crash' (#37) from io/sexp into dev
Reviewed-on: #37
2023-12-07 12:33:01 -08:00
Leni Aniva 924a67f46d doc: getUsedConstants bug about projections 2023-12-06 15:05:04 -08:00
Leni Aniva 8a8db545a5 fix: Printing projection leads to crash 2023-12-05 22:45:59 -08:00
Leni Aniva f2b54ec018 Merge pull request 'feat: Handling of private names' (#36) from library/catalog into dev
Reviewed-on: #36
2023-12-05 20:22:38 -08:00
Leni Aniva 3c2d93259f Merge branch 'dev' into library/catalog 2023-12-05 20:21:22 -08:00
Leni Aniva 079f12d6d3 chore: Version bump 2023-12-05 20:21:07 -08:00