Commit Graph

226 Commits

Author SHA1 Message Date
Leni Aniva 664516f148
Merge branch 'dev' into bug/env-add-level 2025-03-29 15:44:53 -07:00
Leni Aniva 91fbc4cdca
chore: Remove redundant code 2025-03-29 15:43:49 -07:00
Leni Aniva 2885671490
test: Update LSpec 2025-03-29 15:22:31 -07:00
Leni Aniva b9ff9e8f13
feat(repl): Optional type argument in `env.add` 2025-03-29 14:51:35 -07:00
Leni Aniva 9ea099827f
fix(env): Adding declarations with universe levels 2025-03-29 14:39:42 -07:00
Leni Aniva 0528a1592e
fix: Print internal exceptions nicely 2025-03-28 21:31:30 -07:00
Leni Aniva 4610348fed
feat: `CoreM` timeout 2025-03-28 20:42:10 -07:00
Leni Aniva 9980fd9c39
test(repl): Environment loading from header 2025-03-28 18:45:58 -07:00
Leni Aniva c2b7501649
refactor: Remove `CoreM` from `MainM` 2025-03-28 00:50:39 -07:00
Leni Aniva d305918bb9
chore: Update Lean to v4.17.0 2025-03-24 17:57:34 -07:00
Leni Aniva a28ad9b239
feat(delate): Expand matcher applications 2025-03-17 10:47:11 -07:00
Leni Aniva 8063039f7e Merge pull request 'feat(frontend): Alternative methods of initializing environment' (#173) from frontend/env-init into dev
Reviewed-on: #173
2025-03-14 16:48:40 -07:00
Leni Aniva ef165b7045
fix(frontend): Test update 2025-03-14 16:47:46 -07:00
Leni Aniva 8797bbe245
test(frontend): Fix the open test 2025-03-14 16:35:12 -07:00
Leni Aniva 896475848b
fix: Name generation not available due to context 2025-03-10 19:03:14 -07:00
Leni Aniva 0cfd73e44e
test(frontend): Add scope `open` test 2025-03-09 23:29:33 -07:00
Leni Aniva 7ae50696ac
merge: branch 'dev' into chore/cleanup 2025-03-08 21:18:45 -08:00
Leni Aniva 999bb146fa
chore: Remove all unused auxiliary tactics 2025-03-01 20:12:30 -08:00
Leni Aniva aac39ca60c
fix: Some test errors 2025-02-23 14:13:44 -08:00
Leni Aniva 6a7830cb71
fix: Remove spurious print 2025-01-24 19:24:54 -08:00
Leni Aniva 787c9e606d
chore: Cleanup REPL loop 2025-01-24 19:22:58 -08:00
Leni Aniva 418d630255
fix: Remove unused variable 2025-01-24 19:06:07 -08:00
Leni Aniva 6f792b0657
Merge branch 'dev' into bug/expr-proj-to-app-panic 2025-01-24 15:03:13 -08:00
Leni Aniva be8dee6731
test: Add test for module read 2025-01-24 15:00:35 -08:00
Leni Aniva 5c1e7599c0
feat: Projection export function 2025-01-24 14:44:09 -08:00
Leni Aniva 8ce4cbdcf5
feat: Printing field projection in sexp 2025-01-22 13:01:47 -08:00
Leni Aniva 3a26bb1924
fix: Analyze projection application 2025-01-22 12:49:33 -08:00
Leni Aniva 5994f0ddf0
fix: Conditional handling of `.proj` 2025-01-17 23:10:03 -08:00
Leni Aniva 60e78b322e
fix: Test failures 2025-01-13 12:28:16 -08:00
Leni Aniva 5e61282660
test: Source location extraction 2025-01-13 10:30:26 -08:00
Leni Aniva 9d2a999a4f
merge: branch 'dev' into misc/version 2025-01-13 10:29:50 -08:00
Leni Aniva 6a9ba4bb15
Merge branch 'dev' into goal/tactic-draft 2025-01-13 10:22:05 -08:00
Leni Aniva 9eec14503a
Merge branch 'dev' into bug/incorrect-binder-capture 2025-01-10 12:48:18 -08:00
Leni Aniva 814f36eb63 Merge pull request 'feat: Add source location extraction' (#154) from env/inspect into dev
Reviewed-on: #154
2025-01-10 12:47:35 -08:00
Leni Aniva 4a4b02d7b0
test: Source location extraction 2025-01-10 12:47:13 -08:00
Leni Aniva aa066b8634
fix: Add test 2025-01-08 22:53:10 -08:00
Leni Aniva 072d351f04
fix: Delete extraneous test 2025-01-08 22:47:08 -08:00
Leni Aniva cb46b47a60
test: Draft tactic test 2025-01-08 22:23:30 -08:00
Leni Aniva f891960362
fix: Volatile test 2025-01-07 17:52:28 -08:00
Leni Aniva 6302b747b8
feat: Improve error message clarity 2025-01-07 17:51:32 -08:00
Leni Aniva 524314721b
feat: Gate type error collection behind flag 2025-01-07 19:40:03 +09:00
Leni Aniva 5a05e9e8d4
test: Add binder capturing test 2024-12-22 08:47:38 +09:00
Leni Aniva 53bad1c4c9
refactor: Remove obsolete sanitize option 2024-12-15 12:52:08 -08:00
Leni Aniva 7a3b89cc0e
feat: Simplify sexp binder 2024-12-15 12:49:02 -08:00
Leni Aniva 13e01b9e62
Merge branch 'dev' into misc/version 2024-12-11 20:53:32 -08:00
Leni Aniva 2f732a7f20
feat: Print goals in `goal.print` 2024-12-11 16:49:52 -08:00
Leni Aniva 7cba8efd54
Merge branch 'dev' into frontend/infotree 2024-12-11 01:14:15 -08:00
Leni Aniva 1527743900
refactor: Optionalize CompilationUnit 2024-12-09 21:00:33 -08:00
Leni Aniva eb0374dfb3
feat: Collect new constants in repl 2024-12-09 20:57:25 -08:00
Leni Aniva 9a69c48cb2
fix: Integration test failure 2024-12-09 20:42:05 -08:00