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 |