Commit Graph

553 Commits

Author SHA1 Message Date
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 c1f63af019 chore: Update version to 0.2.25 2025-01-13 12:29:11 -08:00
Leni Aniva b8b46c4a9c Merge pull request 'chore: Update Lean to v4.15.0' (#134) from misc/version into dev
Reviewed-on: #134
2025-01-13 12:28:49 -08:00
Leni Aniva 60e78b322e
fix: Test failures 2025-01-13 12:28:16 -08:00
Leni Aniva 06fdf7e678
chore: Update Lean to v4.15.0 2025-01-13 11:09:55 -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 db24650aec Merge pull request 'feat: Draft tactic' (#153) from goal/tactic-draft into dev
Reviewed-on: #153
2025-01-13 10:22:35 -08:00
Leni Aniva 6a9ba4bb15
Merge branch 'dev' into goal/tactic-draft 2025-01-13 10:22:05 -08:00
Leni Aniva ebde7c9eed
feat: Prohibit coupling in drafting 2025-01-13 10:20:36 -08:00
Leni Aniva ef4e5ecbf8
chore: Update version 2025-01-10 12:55:26 -08:00
Leni Aniva a374af3a5f Merge pull request 'fix: Incorrect binder capture' (#152) from bug/incorrect-binder-capture into dev
Reviewed-on: #152
2025-01-10 12:49:14 -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 97eaadc93c
feat: Add source location extraction 2025-01-10 12:16:23 -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 5ce6123de7
feat: Draft tactic 2025-01-08 19:56:14 -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 07e737eb81 Merge pull request 'feat: Simplify sexp printing' (#149) from delate/sexp into dev
Reviewed-on: #149
2025-01-07 17:31:29 -08:00
Leni Aniva 56f40462ae Merge pull request 'fix: Unnecessary instantiation call' (#148) from goal/tactic into dev
Reviewed-on: #148
2025-01-07 17:31:08 -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 48b924fae2
fix(frontend): Incorrect capture of binder term 2024-12-20 19:12:12 +09:00
Leni Aniva b42d917aa7
fix: Unnecessary instantiation call 2024-12-17 08:18:27 +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 c0090dec97
fix: Quote string literal in sexp 2024-12-15 12:40:47 -08:00
Leni Aniva 13e01b9e62
Merge branch 'dev' into misc/version 2024-12-11 20:53:32 -08:00
Leni Aniva 3744cfaa96 Merge pull request 'feat: Print value of arbitrary mvar and goals in goal state' (#141) from goal/print into dev
Reviewed-on: #141
2024-12-11 16:52:19 -08:00
Leni Aniva 0fa57a5a15
Merge branch 'dev' into goal/print 2024-12-11 16:51:58 -08:00
Leni Aniva b9c114fe21 Merge pull request 'doc: Add limitations' (#145) from doc/rationale into dev
Reviewed-on: #145
2024-12-11 16:51:23 -08:00
Leni Aniva 2f732a7f20
feat: Print goals in `goal.print` 2024-12-11 16:49:52 -08:00
Leni Aniva eeb336c944
Merge branch 'dev' into goal/print 2024-12-11 16:40:01 -08:00
Leni Aniva bb445f4d73
chore: Update version 2024-12-11 16:38:59 -08:00
Leni Aniva f111da7de7
doc: Add limitations 2024-12-11 15:09:14 -08:00
Leni Aniva fecab387dc
merge: branch 'dev' into doc/rationale 2024-12-11 15:05:09 -08:00
Leni Aniva f14a37897b Merge pull request 'fix: Reset core message log' (#144) from bug/core-state-error-linger into dev
Reviewed-on: #144
2024-12-11 09:09:33 -08:00
Leni Aniva 396a787771
feat: Reset message log in MainM 2024-12-11 09:06:42 -08:00
Leni Aniva ab77418e24
fix: Drop previous message lists 2024-12-11 09:05:47 -08:00
Leni Aniva f2f71a6028
fix: Reset core message log 2024-12-11 09:01:57 -08:00
Leni Aniva 5d76626912 Merge pull request 'feat: Extract type error and new constants' (#128) from frontend/infotree into dev
Reviewed-on: #128
2024-12-11 01:25:35 -08:00
Leni Aniva 7cba8efd54
Merge branch 'dev' into frontend/infotree 2024-12-11 01:14:15 -08:00
Leni Aniva e9fbce7b4d Merge pull request 'fix: Tactic failure on synthesizing placeholder' (#139) from bug/tactic-failure-placeholder into dev
Reviewed-on: #139
2024-12-11 01:13:14 -08:00
Leni Aniva 4217dbcf80
Merge branch 'dev' into bug/tactic-failure-placeholder 2024-12-11 01:08:44 -08:00