Leonardo de Moura
|
dd4fb3b71b
|
chore: improve error message
see #346
|
2021-03-16 20:42:38 -07:00 |
|
Leonardo de Moura
|
6d53202e0b
|
chore: fix typo
|
2021-03-16 19:07:35 -07:00 |
|
Leonardo de Moura
|
08f87752ee
|
fix: closes #346
|
2021-03-16 18:55:46 -07:00 |
|
Leonardo de Moura
|
97b2398972
|
chore: cleanup
|
2021-03-16 18:14:27 -07:00 |
|
Leonardo de Moura
|
60a1b828ad
|
fix: fixes #348
|
2021-03-16 17:50:40 -07:00 |
|
Leonardo de Moura
|
1fd8089d19
|
fix: register new metavariables created when applying default instance
closes #353
|
2021-03-16 17:31:51 -07:00 |
|
Leonardo de Moura
|
c37d961fc3
|
chore: make sure both alternatives use throwError
|
2021-03-16 17:20:00 -07:00 |
|
Leonardo de Moura
|
7dc6721fea
|
fix: missing pushScope and popScope
|
2021-03-16 16:42:45 -07:00 |
|
Sebastian Ullrich
|
99d8e34a51
|
feat: server: highlight variables & field notation
|
2021-03-16 16:41:32 -07:00 |
|
Sebastian Ullrich
|
8a5344ed17
|
fix: server: handle requests for closed files
|
2021-03-16 16:41:32 -07:00 |
|
Sebastian Ullrich
|
002efd0db6
|
chore: server: exclude some nodes from semantic highlighting
|
2021-03-16 16:41:32 -07:00 |
|
Sebastian Ullrich
|
0e8272388d
|
fix: server: semantic highlighting with multiple tokens in a line
|
2021-03-16 16:41:32 -07:00 |
|
Sebastian Ullrich
|
bddf2ca7e1
|
chore: Nix: update vscode-lean4
|
2021-03-16 16:41:32 -07:00 |
|
Sebastian Ullrich
|
92f75cf37b
|
feat: lean4-mode: enable semantic tokens by default
|
2021-03-16 16:41:32 -07:00 |
|
Sebastian Ullrich
|
cb5050bb7f
|
doc: Syntax.topDown
|
2021-03-16 16:41:32 -07:00 |
|
Sebastian Ullrich
|
ddff87f7f5
|
feat: server: also implement full semantic token requests
because lsp-mode freaks out without them
|
2021-03-16 16:41:32 -07:00 |
|
Sebastian Ullrich
|
5df753f338
|
feat: server: support ranged semantic tokens (keywords only for now)
|
2021-03-16 16:41:32 -07:00 |
|
Leonardo de Moura
|
89797c4485
|
chore: improve congrDefault
We don't need `congrMatch` anymore.
|
2021-03-16 15:59:11 -07:00 |
|
Leonardo de Moura
|
8227d3afcd
|
feat: support for simplifying match discriminants
|
2021-03-16 15:51:36 -07:00 |
|
Leonardo de Moura
|
2970c6ca79
|
feat: add mkCongrDepArg and mkCongrDep
|
2021-03-16 15:40:48 -07:00 |
|
Leonardo de Moura
|
0fd9b493fa
|
chore: add helper congruence lemma
|
2021-03-16 15:40:28 -07:00 |
|
Leonardo de Moura
|
ea91317f1a
|
fix: avoid nontermination due to respecialization
|
2021-03-15 19:12:57 -07:00 |
|
Leonardo de Moura
|
cc0712fc82
|
feat: add support for offset terms at DiscrTree
|
2021-03-14 08:23:44 -07:00 |
|
Sebastian Ullrich
|
75a97fad94
|
feat: nicer token parse errors
|
2021-03-14 08:23:32 -07:00 |
|
Sebastian Ullrich
|
9f21d6fd64
|
fix: preserve token parse errors
|
2021-03-14 08:23:32 -07:00 |
|
Sebastian Ullrich
|
048d592fe8
|
fix: FileMap out of bounds
|
2021-03-14 08:23:32 -07:00 |
|
Leonardo de Moura
|
12aa5cc461
|
chore: avoid ! in keywords
|
2021-03-13 17:24:27 -08:00 |
|
Leonardo de Moura
|
e04e9ff87e
|
feat: extend anonymous ctor notation
|
2021-03-13 17:11:37 -08:00 |
|
Leonardo de Moura
|
c54a7c8ccc
|
chore: make HasEquiv more general
|
2021-03-13 07:02:35 -08:00 |
|
Sebastian Ullrich
|
d35fc280d2
|
refactor: further refactor Lean.Elab.Syntax
|
2021-03-13 14:47:59 +01:00 |
|
Sebastian Ullrich
|
00a0db4231
|
fix: unexpanders should inherit scopedness
|
2021-03-13 13:20:12 +01:00 |
|
Sebastian Ullrich
|
8f824ce141
|
fix: KeyedDeclsAttribute: preserve scopedness
|
2021-03-13 13:18:04 +01:00 |
|
Sebastian Ullrich
|
03aea90981
|
chore: update stage0
|
2021-03-13 12:41:13 +01:00 |
|
Sebastian Ullrich
|
d88ef52b68
|
feat: scoped KeyedDeclsAttribute
|
2021-03-13 12:40:58 +01:00 |
|
Sebastian Ullrich
|
fb4d07de49
|
chore: lean4-mode: use proper hook for goal refresh
debounced and should wait until after initialization
|
2021-03-13 12:20:52 +01:00 |
|
Leonardo de Moura
|
5c24906c60
|
fix: Delaborator for constants
@Kha Could you please take a look at the fix?
This is an example posted by @JasonGross on Zulip.
|
2021-03-12 19:51:27 -08:00 |
|
Leonardo de Moura
|
a406e41fcb
|
chore: fix documentation
|
2021-03-12 18:11:06 -08:00 |
|
Leonardo de Moura
|
fb40b5e80d
|
chore: fix test
|
2021-03-12 18:07:58 -08:00 |
|
Leonardo de Moura
|
75051778ce
|
chore: update stage0
|
2021-03-12 18:02:53 -08:00 |
|
Leonardo de Moura
|
a30a256123
|
refactor: remove Tactic/Binders.lean
These macro expansion functions can be now implemented using `macro` and `macro_rules`.
|
2021-03-12 17:59:21 -08:00 |
|
Leonardo de Moura
|
50fd39db89
|
fix: bug at allGoals
|
2021-03-12 17:48:33 -08:00 |
|
Leonardo de Moura
|
a7c5db6d21
|
chore: update stage0
|
2021-03-12 17:41:06 -08:00 |
|
Leonardo de Moura
|
1df84e3a6d
|
feat: allow haveDecl, sufficesDecl, letRecDecls in antiquotations
|
2021-03-12 17:40:16 -08:00 |
|
Leonardo de Moura
|
d330f1e2e2
|
feat: rotateLeft and rotateRight tactics
|
2021-03-12 17:13:03 -08:00 |
|
Leonardo de Moura
|
27e15961cd
|
fix: no coercions at exact and refine
|
2021-03-12 17:12:25 -08:00 |
|
Leonardo de Moura
|
091fadbf64
|
feat: add List.rotateLeft and List.rotateRight
|
2021-03-12 17:09:22 -08:00 |
|
Leonardo de Moura
|
7627458aac
|
chore: fix tests
We are not using the `!` suffix anymore for keywords.
|
2021-03-12 15:10:50 -08:00 |
|
Leonardo de Moura
|
3d58c4d115
|
chore: remove old notation
|
2021-03-12 15:05:06 -08:00 |
|
Leonardo de Moura
|
5eb0a7a4fc
|
chore: update stage0
|
2021-03-12 14:58:44 -08:00 |
|
Leonardo de Moura
|
bf8119a5cd
|
chore: convert keywords to snake_case
Again `!` is only for functions that can panic.
|
2021-03-12 13:34:51 -08:00 |
|