lean4-htt/src/Lean/Data
2021-01-13 18:31:41 -08:00
..
Json fix: encode none optional JSON fields as missing 2021-01-02 14:13:22 -05:00
Lsp feat: server: report document symbol hierarchy 2020-12-31 15:00:59 +01:00
Format.lean refactor: Repr 2020-12-18 11:21:30 -08:00
Json.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
JsonRpc.lean test: multi-process server 2020-12-26 13:22:47 +01:00
KVMap.lean chore: user deriving BEq 2020-12-13 16:30:07 -08:00
LBool.lean chore: user deriving BEq 2020-12-13 16:30:07 -08:00
LOption.lean chore: user deriving BEq 2020-12-13 16:30:07 -08:00
Lsp.lean chore: Hover.lean ~> LanguageFeatures.lean 2020-12-31 15:00:42 +01:00
Name.lean chore: use deriving Inhabited 2020-12-13 11:57:59 -08:00
NameTrie.lean feat: trie for hierarchical names 2020-12-03 16:40:00 -08: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 chore: adjust instance param order 2021-01-13 18:31:41 -08:00
Position.lean feat: store declaration ranges 2021-01-11 12:50:11 -08:00
PrefixTree.lean feat: trie for hierarchical names 2020-12-03 16:40:00 -08:00
SMap.lean chore: update structure, class, inductive 2020-11-27 15:09:30 -08:00
Trie.lean refactor: move Format to Init package 2020-12-18 11:21:30 -08:00