lean4-htt/src/Lean/Data
2021-10-08 11:28:04 +02:00
..
Json refactor: use JSON to communicate between server & package manager 2021-10-08 11:28:04 +02:00
Lsp feat: add enum command for declaring enumeration types 2021-09-05 16:58:49 -07:00
Xml feat: add xml parser. 2021-07-13 09:58:27 -07:00
Format.lean chore: restore non-generic Format 2021-08-01 09:58:44 +02:00
Json.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
JsonRpc.lean refactor: make lsp/release a notification 2021-08-01 09:58:44 +02:00
KVMap.lean feat: set_option completion 2021-04-03 15:06:50 -07:00
LBool.lean chore: user deriving BEq 2020-12-13 16:30:07 -08:00
LOption.lean chore: fix codebase and tests 2021-06-29 17:14:52 -07:00
Lsp.lean chore: Hover.lean ~> LanguageFeatures.lean 2020-12-31 15:00:42 +01:00
Name.lean refactor: move lean_name_eq to runtime, add lean_name_hash in C 2021-08-16 16:13:55 -07:00
NameTrie.lean refactor: use Ordering inside of rbmap instead of lt. 2021-04-27 07:58:58 -07:00
Occurrences.lean chore: user deriving BEq 2020-12-13 16:30:07 -08:00
OpenDecl.lean chore: update structure, class, inductive 2020-11-27 15:09:30 -08:00
Options.lean feat: add withOptions 2021-09-17 14:20:28 -07:00
Parsec.lean refactor: lazy evaluation for <|> 2021-09-07 17:06:10 -07:00
Position.lean fix: index out of bounds 2021-08-12 05:39:19 -07:00
PrefixTree.lean refactor: use Ordering inside of rbmap instead of lt. 2021-04-27 07:58:58 -07:00
Rat.lean chore: cleanup 2021-09-14 19:20:32 -07:00
SMap.lean refactor: lazy evaluation for <|> 2021-09-07 17:06:10 -07:00
SSet.lean feat: add "staged set" helper type 2021-07-31 14:23:29 -07:00
Trie.lean refactor: use Ordering inside of rbmap instead of lt. 2021-04-27 07:58:58 -07:00
Xml.lean feat: add xml parser. 2021-07-13 09:58:27 -07:00