Commit Graph

27 Commits

Author SHA1 Message Date
Leni Aniva 737fd607e8
refactor: Add heuristic case to `isAuxLemma` 2025-07-02 14:54:13 -07:00
Leni Aniva 9a9659fdb2
feat(delate): Show fragments for each goal 2025-06-26 14:22:51 -07:00
Leni Aniva 0b731273b2
refactor(goal): A state can have multiple parents 2025-06-25 13:07:47 -07:00
Leni Aniva 7d9d3e4742
fix: Use the correct unfold aux lemma 2025-06-19 15:48:53 -07:00
Leni Aniva 60f79f5f02
doc: Fix typo 2025-04-14 23:26:14 -07:00
Leni Aniva b6c3f7d8fd
chore: Update Lean to v4.18.0 2025-04-08 10:58:38 -07:00
Leni Aniva d305918bb9
chore: Update Lean to v4.17.0 2025-03-24 17:57:34 -07:00
Leni Aniva cb1082c7c7
chore: More code cleanup 2025-03-17 12:14:16 -07:00
Leni Aniva 678cc9b3c0
chore: Code cleanup 2025-03-17 11:30:24 -07:00
Leni Aniva 4643992c3b
refactor(delate): Unfold matchers into function 2025-03-17 11:26:13 -07:00
Leni Aniva 3b4b196a30
feat(delate): Add mdata annotation for matcher 2025-03-17 11:20:38 -07:00
Leni Aniva a28ad9b239
feat(delate): Expand matcher applications 2025-03-17 10:47:11 -07:00
Leni Aniva dc29d48b77
chore: Remove IO.println for trace 2025-03-17 09:31:39 -07:00
Leni Aniva 98ad1ae283
feat(delate): Tracing tags 2025-03-14 16:54:34 -07: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 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 44aef76a10
refactor: Remove sanitization for mvarId/fvarId 2024-11-26 12:57:19 -08:00
Leni Aniva a8e7a1a726
feat: Erase macro scopes in sexp 2024-11-26 12:34:52 -08:00
Leni Aniva ee8063e1f5
refactor: Merge all Delation functions 2024-11-08 14:41:24 -08:00
Leni Aniva 70f86f6e93
doc: Update delation documentation 2024-11-08 14:34:15 -08:00
Leni Aniva 0d57027681
refactor: Merge Condensed into Delate 2024-11-08 13:05:48 -08:00
Leni Aniva 1c4f38e5eb
refactor: Rename {Serial,Delate}.lean 2024-11-08 13:04:00 -08:00