 Leni Aniva
|
aa122b2bb9
|
doc: Update rationale link
|
2024-12-11 00:24:56 -08:00 |
|
Leni Aniva
|
4bd50c17ac
|
Merge branch 'dev' into doc/rationale
|
2024-12-05 17:23:32 -08:00 |
|
Leni Aniva
|
d00e376943
|
doc: Remove outdated documentation
|
2024-12-05 17:18:35 -08:00 |
|
Leni Aniva
|
3da85b7f04
|
doc: Documentation for save/load
|
2024-12-05 16:00:46 -08:00 |
|
Leni Aniva
|
5d676154f1
|
doc: Fix documentation link
|
2024-11-16 21:27:40 -08:00 |
|
Leni Aniva
|
ce3af887be
|
doc: Rationale document
|
2024-11-15 23:36:28 -08:00 |
|
Leni Aniva
|
f729a357b9
|
Merge branch 'dev' into frontend/collect-holes
|
2024-09-09 17:35:10 -07:00 |
|
Leni Aniva
|
9075ded885
|
feat: Set `automaticMode` to true by default
|
2024-09-09 17:29:43 -07:00 |
|
Leni Aniva
|
9f0de0957e
|
doc: Update documentation for frontend command
|
2024-09-09 12:39:32 -07:00 |
|
Leni Aniva
|
e2ad6ce6b3
|
doc: Documentation for automatic mode
|
2024-09-06 21:32:02 -07:00 |
|
Leni Aniva
|
76765c913c
|
test: Use `lake test`. Retired `Makefile`
|
2024-08-18 12:22:59 -07:00 |
|
Leni Aniva
|
773a0afbd8
|
feat: Handling of universe level names in elab
|
2024-06-11 12:44:42 -07:00 |
|
Leni Aniva
|
7531ad628c
|
doc: Documentation about conditional arguments
|
2024-04-15 20:00:59 -07:00 |
|
Leni Aniva
|
52e5b5df50
|
doc: README.md fix
|
2024-04-15 19:57:05 -07:00 |
|
Leni Aniva
|
ed220bc7fb
|
doc: New tactics in README.md
|
2024-04-11 15:13:12 -07:00 |
|
Leni Aniva
|
042dc8f530
|
doc: Documentation for `nix flake check`
|
2024-04-06 14:15:58 -07:00 |
|
Leni Aniva
|
f462843218
|
docs: Update README.md
|
2024-03-31 16:12:23 -07:00 |
|
Leni Aniva
|
4a89aaf70e
|
doc: Main README.md
|
2024-03-28 22:12:11 -07:00 |
|
Leni Aniva
|
47fabf333b
|
doc: Update README.md
|
2024-03-28 11:37:07 -07:00 |
|
Leni Aniva
|
ff4671cdd0
|
chore: Rename lib. commands to env.
This is done to improve clarity and align with Lean's terminology
|
2023-12-12 18:56:25 -08:00 |
|
Leni Aniva
|
c6bb4be597
|
chore: Update documentation
|
2023-11-06 11:04:28 -08:00 |
|
Leni Aniva
|
045181356c
|
feat: Add REPL function for root expression
|
2023-10-27 15:41:12 -07:00 |
|
Leni Aniva
|
a9294e0338
|
Add documentation about flake
|
2023-10-20 12:54:35 -07:00 |
|
Leni Aniva
|
6d15d1e670
|
Use makefile instead of ad-hoc script
|
2023-10-02 10:26:19 -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
|
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
|
ff8fed8741
|
Classify JSON error as command error
Also add documentation for this
|
2023-08-24 22:51:40 -07:00 |
|
Leni Aniva
|
96cbbf2551
|
Add compressed json print option; Rearrange commands into hierarchy
|
2023-08-16 19:25:32 -07:00 |
|
Leni Aniva
|
7771408de1
|
Add expression sexp printing (2/2)
|
2023-08-14 21:43:40 -07:00 |
|
Leni Aniva
|
9eadd1d4d4
|
Add expression sexp printing (1/2, tests pending)
|
2023-08-14 17:07:53 -07:00 |
|
Leni Aniva
|
5cedb9d88c
|
version bump, restructure
|
2023-08-13 21:19:06 -07:00 |
|
Leni Aniva
|
622aa7f969
|
Add documentation; Remove mathlib dependency
|
2023-06-09 14:45:45 -07:00 |
|
Leni Aniva
|
e0c5f76451
|
Rename tactic failure mode to avoid confusion
Clean up README
|
2023-05-24 23:11:17 -07:00 |
|
Leni Aniva
|
1ed1aff7c9
|
Add documentation about options
|
2023-05-24 00:55:54 -07:00 |
|
Leni Aniva
|
1fed222f56
|
Use TermElabM as the main monad stack instead of IO
|
2023-05-23 05:12:46 -07:00 |
|
Leni Aniva
|
ba779766c0
|
Rename ids so they are consistent
|
2023-05-22 19:51:16 -07:00 |
|
Leni Aniva
|
1ad45f650f
|
Remove testing stub in README.md
|
2023-05-22 19:12:07 -07:00 |
|
Leni Aniva
|
6a71dad389
|
Add option format for proof output and test cases
|
2023-05-22 14:49:56 -07:00 |
|
Leni Aniva
|
46ccad1669
|
Add default arguments for Json
|
2023-05-22 00:49:37 -07:00 |
|
Leni Aniva
|
083ec8beec
|
Add REPL tactics
|
2023-05-21 17:41:39 -07:00 |
|
Leni Aniva
|
15aab3d31f
|
Remove ExceptT from main monad
Allow pretty printing of expr
|
2023-05-20 15:58:38 -07:00 |
|
Leni Aniva
|
2a4d348aab
|
Add expression IO stub for constant types
|
2023-05-20 14:04:09 -07:00 |
|
Leni Aniva
|
8127e9ba06
|
Add alternative command input format and IO stub
|
2023-05-20 13:03:12 -07:00 |
|
Leni Aniva
|
4d636ec12b
|
Add stack size troubleshooting
|
2023-05-14 15:22:41 -07:00 |
|
Leni Aniva
|
d3af535652
|
Add unsafe filtering in catalog
|
2023-05-12 16:12:21 -07:00 |
|
Leni Aniva
|
7c96479bb5
|
Add working catalog code and example
|
2023-05-12 01:08:36 -07:00 |
|
Leni Aniva
|
b5cb464694
|
Add README and catalog functions
|
2023-05-09 22:51:19 -07:00 |