Leni Aniva
d35803791e
Merge branch 'dev' into goal/continuation
2023-11-07 12:11:14 -08:00
Leni Aniva
d9745094fa
fix: Remove the error prone SemihashMap
2023-11-07 12:09:54 -08:00
Leni Aniva
53b63bf46c
fix: Remove the error prone SemihashMap
2023-11-07 12:04:17 -08:00
Leni Aniva
4396da3e65
chore: Code formatting
2023-11-06 12:20:08 -08:00
Leni Aniva
ce585f7288
feat: Print the root mvar name
2023-11-06 11:51:31 -08:00
Leni Aniva
32fedede6a
Merge branch 'dev' into goal/continuation
2023-11-06 11:45:24 -08:00
Leni Aniva
8182da436d
chore: Remove unnecessary unsafe's
2023-11-06 11:43:57 -08:00
Leni Aniva
c6bb4be597
chore: Update documentation
2023-11-06 11:04:28 -08:00
Leni Aniva
ce1cb13e54
fix: Use Lean's built in name parser
...
The `str_to_name` parser cannot handle numerical names and escapes.
2023-11-06 10:45:11 -08:00
Leni Aniva
a5b5e01858
chore: Version bump to 0.2.8
2023-11-04 15:54:28 -07:00
Leni Aniva
4be9dbc84a
feat: Goal continuation fails if target has goals
2023-11-04 15:53:57 -07:00
Leni Aniva
97d658cfc5
feat: Add goal.continue command
2023-11-04 15:51:09 -07:00
Leni Aniva
333355a85d
feat: Partial state continuation
2023-11-04 15:33:53 -07:00
Leni Aniva
4a4a33cea7
test: Separate mvar coupling tests
2023-11-04 15:01:41 -07:00
Leni Aniva
1638c308a9
Merge pull request 'feat: Minor updates to serialization' ( #26 ) from io/serial into dev
...
Reviewed-on: #26
2023-10-30 14:47:41 -07:00
Leni Aniva
59ac83f0b7
bug: Fix quote escape problem
2023-10-30 14:45:43 -07:00
Leni Aniva
d1c0dc376f
feat: Print metavariable name in goal
2023-10-30 14:44:06 -07:00
Leni Aniva
6cf328a84f
Merge pull request 'feat: Simplify printing of names and expressions' ( #25 ) from io/serial into dev
...
Reviewed-on: #25
2023-10-29 13:08:05 -07:00
Leni Aniva
1a99a2e7b2
fix: Sanitize name in universe levels
2023-10-29 13:03:48 -07:00
Leni Aniva
60854525b9
feat: Simplify printing of function applications
2023-10-29 12:50:36 -07:00
Leni Aniva
e523e8bcc6
chore: Version bump (breaking change)
2023-10-29 11:57:24 -07:00
Leni Aniva
de250eafd0
feat: Print names in one segment separated with .
2023-10-29 11:56:56 -07:00
Leni Aniva
c0dfa04b18
feat: Simplify name printing
2023-10-29 11:18:35 -07:00
Leni Aniva
4ce932eb3b
Merge pull request 'Enable handling of m-Coupled goals' ( #20 ) from goal/dependency into dev
...
Reviewed-on: #20
2023-10-27 19:30:20 -07:00
Leni Aniva
045181356c
feat: Add REPL function for root expression
2023-10-27 15:41:12 -07:00
Leni Aniva
41e1f64d44
Merge branch 'dev' into goal/dependency
2023-10-27 15:33:47 -07:00
Leni Aniva
3b1746490d
feat: Add REPL command for assigning an expression
2023-10-27 15:32:59 -07:00
Leni Aniva
f064bb21a4
feat: Assigning a goal with an expression
2023-10-27 15:15:22 -07:00
Leni Aniva
269e5c707c
refactor: Separate goal printing and processing
...
Added a test for delta proof variables
2023-10-26 22:47:42 -07:00
Leni Aniva
c852db2f46
test: m-coupled goals
2023-10-26 11:22:02 -07:00
Leni Aniva
8029298db7
feat: Display user name in Goal structure
...
1. Modify `serialize_expression_ast` so its no longer a monad
2. Test existence of root expression
2023-10-25 22:18:59 -07:00
Leni Aniva
d991533170
feat: Add proof continue and root extraction
2023-10-25 16:03:45 -07:00
Leni Aniva
a9294e0338
Add documentation about flake
2023-10-20 12:54:35 -07:00
Leni Aniva
3d7d5d6b4d
feat: Add nix flake
2023-10-20 12:41:56 -07:00
Leni Aniva
538ba6e7d7
Store states instead of goals
...
1. Rename {Commands, Protocol}, and {Symbols, Symbol}
2. Store the root mvarId in the proof state along with goal indices
3. Add diagnostics function which prints out the state
4. Bump version to 0.2.6 (breaking change)
Documentations pending
2023-10-15 17:15:23 -07:00
Leni Aniva
41db295ff5
Rename tactic to goal and restructure
2023-10-15 12:31:22 -07:00
Leni Aniva
7a5fe554ba
Add holes test stub
...
Move tests into their own namespaces
2023-10-06 17:31:36 -07:00
Leni Aniva
13f3460e9a
Fix test failures
2023-10-05 17:51:41 -07:00
Leni Aniva
a8cf94ccb1
Bump Lean version to 4.1.0
2023-10-05 17:49:43 -07:00
Leni Aniva
0948e71d60
Add dependency for lakefile and lean-toolchain
2023-10-02 10:30:58 -07:00
Leni Aniva
6d15d1e670
Use makefile instead of ad-hoc script
2023-10-02 10:26:19 -07:00
Leni Aniva
35b391881e
Add ready message to indicate the main loop is up
2023-10-02 10:14:03 -07:00
Leni Aniva
d7077ce854
Bump lean version to 4.0.0
2023-09-13 21:02:26 -07:00
Leni Aniva
75f43786fb
Merge pull request 'Simplify goal bookkeeping mechanism' ( #10 ) from tactic/book into dev
...
Reviewed-on: #10
2023-08-30 19:18:36 -07:00
Leni Aniva
f538f580bd
Merge branch 'dev' into tactic/book
2023-08-30 19:17:25 -07:00
Leni Aniva
f1f1c20ff9
Add SemihashMap interface, rename proof commands to goal commands, allow deletion
2023-08-30 19:16:33 -07:00
Leni Aniva
6b96f7893f
Separate max and imax in sort level
2023-08-27 22:50:18 -07:00
Leni Aniva
b98304f78a
Version bump to 0.2.4 due to breaking change
2023-08-27 19:59:31 -07:00
Leni Aniva
a6e337a89e
Rename proof commands to goal commands
2023-08-27 19:58:52 -07:00
Leni Aniva
a86af1bc57
Add SemihashMap structure for goal bookkeeping
2023-08-27 19:53:09 -07:00
Leni Aniva