|
Json
|
chore: adapt to upstream
|
2020-08-31 06:50:01 -07:00 |
|
Lsp
|
refactor: move ppExpr to IO
|
2020-09-15 18:48:21 -07:00 |
|
Format.lean
|
chore: use [builtinInit]
|
2020-10-19 14:58:38 -07:00 |
|
Json.lean
|
chore: adapt to upstream
|
2020-08-31 06:50:01 -07:00 |
|
JsonRpc.lean
|
chore: adapt to upstream
|
2020-08-31 06:50:01 -07:00 |
|
KVMap.lean
|
chore: move to new frontend
|
2020-10-20 11:12:42 -07:00 |
|
LBool.lean
|
chore: move to new frontend
|
2020-10-20 11:19:44 -07:00 |
|
Lsp.lean
|
chore: copyright
|
2020-08-31 06:50:01 -07:00 |
|
Name.lean
|
fix: NameSet.insert return type
|
2020-09-29 07:59:22 -07:00 |
|
Occurrences.lean
|
chore: move to new frontend
|
2020-10-20 11:19:44 -07:00 |
|
OpenDecl.lean
|
chore: move to new frontend
|
2020-10-20 11:19:44 -07:00 |
|
Options.lean
|
chore: move to new frontend
|
2020-10-20 11:19:44 -07:00 |
|
Trie.lean
|
chore: move RBTree and RBMap to Std
|
2020-06-25 13:26:16 -07:00 |