Leni Aniva
cf856d2880
chore: Version bump
2023-12-05 20:21:07 -08:00
Leni Aniva
beb837ccab
Merge pull request 'feat: Print structural projection as application' ( #35 ) from io/serial into dev
...
Reviewed-on: #35
2023-12-05 20:20:51 -08:00
Leni Aniva
da74258dd1
feat!: Display public name only if name is private
2023-12-05 20:20:08 -08:00
Leni Aniva
9f2b07757f
feat: Display whether a symbol is private
2023-12-05 19:07:00 -08:00
Leni Aniva
07ade4c822
feat: Expose _private names
2023-12-04 23:36:09 -08:00
Leni Aniva
a454aaf1d4
feat: Remove stem deduce
...
Some private subproofs are not shown in the catalog and this breaks
dependencies
2023-12-04 16:40:15 -08:00
Leni Aniva
ec09304e02
feat: Remove printing projections
2023-12-04 16:21:02 -08:00
Leni Aniva
967e3dfb4f
feat: Remove | in symbol output
2023-11-27 09:54:41 -08:00
Leni Aniva
0a5a96275f
chore: Version bump to 0.2.9
2023-11-26 23:48:47 -08:00
Leni Aniva
7690272bfa
feat: Shorter symbol category
2023-11-26 22:14:58 -08:00
Leni Aniva
7b59937853
feat: Read dependencies of library symbols
2023-11-25 15:07:56 -08:00
Leni Aniva
2a9931c134
fix: Rectify error format
2023-11-09 22:24:17 -08:00
Leni Aniva
c99125c4a6
Merge pull request 'feat: Allow selective continuation of goals' ( #27 ) from goal/continuation into dev
...
Reviewed-on: #27
2023-11-07 16:49:55 -08:00
Leni Aniva
8218d3f004
fix: Do not show parent state in continue
2023-11-07 13:10:14 -08:00
Leni Aniva
736e68639f
fix: New goal state not inserted correctly
2023-11-07 13:07:50 -08:00
Leni Aniva
cfd1cfd107
Merge branch 'dev' into goal/continuation
2023-11-07 12:11:14 -08:00
Leni Aniva
764be6d14b
fix: Remove the error prone SemihashMap
2023-11-07 12:09:54 -08:00
Leni Aniva
5ac5198f51
fix: Remove the error prone SemihashMap
2023-11-07 12:04:17 -08:00
Leni Aniva
7076669c3d
chore: Code formatting
2023-11-06 12:20:08 -08:00
Leni Aniva
245e76b2f1
feat: Print the root mvar name
2023-11-06 11:51:31 -08:00
Leni Aniva
7c28cf4ed0
Merge branch 'dev' into goal/continuation
2023-11-06 11:45:24 -08:00
Leni Aniva
c5f563598d
chore: Remove unnecessary unsafe's
2023-11-06 11:43:57 -08:00
Leni Aniva
a7aeb03b43
chore: Update documentation
2023-11-06 11:04:28 -08:00
Leni Aniva
dbace9f2d5
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
782ce38c87
chore: Version bump to 0.2.8
2023-11-04 15:54:28 -07:00
Leni Aniva
d809a960f9
feat: Goal continuation fails if target has goals
2023-11-04 15:53:57 -07:00
Leni Aniva
db706070ad
feat: Add goal.continue command
2023-11-04 15:51:09 -07:00
Leni Aniva
754fb69cff
feat: Partial state continuation
2023-11-04 15:33:53 -07:00
Leni Aniva
dc2cc5be77
test: Separate mvar coupling tests
2023-11-04 15:01:41 -07:00
Leni Aniva
f5ed87f740
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
8dd994d1ca
bug: Fix quote escape problem
2023-10-30 14:45:43 -07:00
Leni Aniva
d87217c6bb
feat: Print metavariable name in goal
2023-10-30 14:44:06 -07:00
Leni Aniva
796f0d8336
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
e5acd4b26c
fix: Sanitize name in universe levels
2023-10-29 13:03:48 -07:00
Leni Aniva
454a5bc6b9
feat: Simplify printing of function applications
2023-10-29 12:50:36 -07:00
Leni Aniva
afed5bbc8d
chore: Version bump (breaking change)
2023-10-29 11:57:24 -07:00
Leni Aniva
e2526f11b1
feat: Print names in one segment separated with .
2023-10-29 11:56:56 -07:00
Leni Aniva
c2d606b9d9
feat: Simplify name printing
2023-10-29 11:18:35 -07:00
Leni Aniva
c19fd1bcfb
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
427d819349
feat: Add REPL function for root expression
2023-10-27 15:41:12 -07:00
Leni Aniva
ca7a081cac
Merge branch 'dev' into goal/dependency
2023-10-27 15:33:47 -07:00
Leni Aniva
82f5494718
feat: Add REPL command for assigning an expression
2023-10-27 15:32:59 -07:00
Leni Aniva
b381d89ff9
feat: Assigning a goal with an expression
2023-10-27 15:15:22 -07:00
Leni Aniva
e98fb77f33
refactor: Separate goal printing and processing
...
Added a test for delta proof variables
2023-10-26 22:47:42 -07:00
Leni Aniva
4ffd226cac
test: m-coupled goals
2023-10-26 11:22:02 -07:00
Leni Aniva
0ecfa9fc26
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
0a0f0304a8
feat: Add proof continue and root extraction
2023-10-25 16:03:45 -07:00
Leni Aniva
7dc6e4e549
Add documentation about flake
2023-10-20 12:54:35 -07:00
Leni Aniva
ba53e9087b
feat: Add nix flake
2023-10-20 12:41:56 -07:00
Leni Aniva
9447d29e37
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