Ed Ayers
0bfee4fe1f
doc: apply suggestions from code review
...
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
2022-07-20 15:30:30 -07:00
E.W.Ayers
64dec36ae3
doc: various docstrings
2022-07-20 15:30:30 -07:00
E.W.Ayers
8fe76ba9f4
doc: prelude Nat, Fin, USize
2022-07-20 15:30:30 -07:00
Sebastian Ullrich
c43a84ca30
fix: unsafe initialize
2022-07-20 22:37:01 +02:00
Sebastian Ullrich
b5417bdc6c
chore: update stage0
2022-07-20 22:12:20 +02:00
Sebastian Ullrich
15bb3ccf6b
chore: reduce TSyntax.Compat scope in Elab.Declaration
2022-07-20 22:12:20 +02:00
Sebastian Ullrich
cdb855d281
feat: support all sensible modifiers on (builtin_)initialize
...
Resolves #1324
2022-07-20 22:12:20 +02:00
Mario Carneiro
a2ef6bd19e
fix: malformed/misaligned markdown code fences
2022-07-20 11:12:42 +02:00
Leonardo de Moura
3846dd60fd
fix: evalTactic
...
This commit fixes bug reported by Patrick Massot.
It happened when using `macro_rules` and `elab_rules` for the same
`SyntaxNodeKind`.
It also fixes missing error messages when there is more than one
elaboration functions and there is `abortTactic` exception.
Remark: this commit also changes the evaluation order. Macros are
now tried before elaboration rules. The motivation is that macros are
already applied before elaboration functions in the term elaborator.
2022-07-19 23:28:14 -04:00
Leonardo de Moura
6558f56c29
fix: rename tactic
2022-07-19 23:28:14 -04:00
Leonardo de Moura
013b9e14f7
chore: fix typo
2022-07-19 23:28:14 -04:00
Gabriel Ebner
f2e7cbfbaf
chore: use inaccessible name for RpcEncodingPacket
2022-07-19 22:55:42 +02:00
Gabriel Ebner
4ce56f7c05
fix: use field names if specified
2022-07-19 22:55:42 +02:00
Gabriel Ebner
59f528e678
fix: support empty inductives in json derive
2022-07-19 22:55:42 +02:00
Gabriel Ebner
2c0f8fac99
feat: support unused params in RpcEncoding deriver
2022-07-19 22:55:42 +02:00
Gabriel Ebner
d36552848c
chore: hide weird RpcEncoding behind Nonempty
2022-07-19 22:55:42 +02:00
Gabriel Ebner
ed5e0f098c
fix: support non-type params in RpcEncoding
2022-07-19 22:55:42 +02:00
Gabriel Ebner
62ede1fdfd
chore: update test
2022-07-19 22:55:42 +02:00
Gabriel Ebner
cde339c2fb
feat: support recursive types in RpcEncoding
2022-07-19 22:55:42 +02:00
Gabriel Ebner
b7bcb1616a
chore: add inhabited instance for RpcEncoding
...
This allows us to define RpcEncodings as partial defs.
2022-07-19 22:55:42 +02:00
Gabriel Ebner
bcf2bf994b
chore: exploit that command* is command as well
2022-07-19 22:55:42 +02:00
Gabriel Ebner
89dfff24ce
chore: avoid $(mkIdent ``foo)
2022-07-19 22:55:42 +02:00
Gabriel Ebner
76e8a40237
chore: pick slightly nicer user-facing names
2022-07-19 22:55:42 +02:00
Gabriel Ebner
8b9c7ebf43
chore: simplify deriveWithRefInstance
2022-07-19 22:55:42 +02:00
Gabriel Ebner
bffd762822
feat: improve RpcEncoding derive test
2022-07-19 22:55:42 +02:00
Gabriel Ebner
c81b10f296
perf: implement Level.update* in Lean
2022-07-19 05:55:13 -07:00
Gabriel Ebner
eda3eae18e
perf: implement Expr.update* in Lean
2022-07-19 05:55:13 -07:00
Sebastian Ullrich
1611cf63c3
fix: make document symbols request deterministic
2022-07-19 12:23:03 +02:00
tydeu
9d4a72bf6a
feat: up to spec SemanticTokens/Type/Modifier
2022-07-19 11:57:57 +02:00
Sebastian Ullrich
987785242f
fix: disable auto implicits in structure field default values
2022-07-18 21:09:56 -07:00
Ed Ayers
2d28a9dd94
doc: explain AttributeKind ( #1316 )
2022-07-18 21:04:18 -07:00
Scott Morrison
5c79973300
feat: allow an ApplyConfig argument at constructor tactic ( #1319 )
2022-07-18 21:02:31 -07:00
Leonardo de Moura
73fce217f6
test: for issue #1321
2022-07-18 23:50:41 -04:00
Leonardo de Moura
678cfda909
chore: update stage0
2022-07-18 23:44:45 -04:00
Leonardo de Moura
e1fc904786
feat: attributes on syntax
...
closes #1321
2022-07-18 23:37:11 -04:00
Leonardo de Moura
3325987be4
chore: fix tests
2022-07-18 23:18:59 -04:00
Leonardo de Moura
d95163641a
chore: indent docstrings
2022-07-18 22:36:55 -04:00
Leonardo de Moura
3691fb2c34
chore: update stage0
2022-07-18 22:29:56 -04:00
Leonardo de Moura
c341d8432f
feat: remove leading spaces from docstrings
2022-07-18 22:18:15 -04:00
Leonardo de Moura
da71dd3d77
chore: docstring
2022-07-18 22:16:32 -04:00
Leonardo de Moura
e8b58abdb2
chore: remove dead code
2022-07-18 22:16:32 -04:00
Sebastian Ullrich
be11e8e29b
doc: missing linebreak
2022-07-18 22:31:16 +02:00
Mac
ad0288d767
feat: allow registering/chaining LSP handlers in initialize
2022-07-18 09:38:30 +02:00
Leonardo de Moura
5083d47e4d
doc: some Syntax
2022-07-17 17:57:33 -04:00
Leonardo de Moura
7331fdf310
doc: Expr.lean
2022-07-17 17:28:28 -04:00
Leonardo de Moura
875b3c84b4
fix: bug at Match.lean
2022-07-17 14:55:57 -04:00
Leonardo de Moura
7cb011e94c
doc: Expr.lean
2022-07-17 14:49:55 -04:00
Leonardo de Moura
2116f69315
chore: unused variables
2022-07-17 13:04:08 -04:00
Gabriel Ebner
3edf22f3f5
fix: crash in binop%
2022-07-17 09:57:56 -07:00
Sebastian Ullrich
8972cc9baf
chore: Nix: cache Leanc-deps
2022-07-16 16:19:01 +02:00
