Leonardo de Moura
|
00ca0dde5c
|
feat: add unop% term parser
We not to support unary minus at `BinOp.toTree`
see #1779
|
2022-10-26 06:19:22 -07:00 |
|
Mario Carneiro
|
765ebcdbf0
|
feat: use withoutPosition consistently
|
2022-10-24 12:51:32 -07:00 |
|
Mario Carneiro
|
e7c7678ab0
|
refactor: line wrapping in parser code
|
2022-10-24 08:37:29 -07:00 |
|
Mario Carneiro
|
b3ba78aade
|
feat: hovers & name resolution in registerCombinatorAttribute (part 2)
|
2022-10-23 09:30:38 +02:00 |
|
Mario Carneiro
|
583e023314
|
chore: snake-case attributes (part 2)
|
2022-10-19 09:28:08 -07:00 |
|
Mario Carneiro
|
dd5948d641
|
chore: snake-case attributes (part 1)
|
2022-10-19 09:28:08 -07:00 |
|
Gabriel Ebner
|
fb4d90a58b
|
feat: dynamic quotations for categories
|
2022-10-18 14:59:14 -07:00 |
|
Gabriel Ebner
|
0d3d05bd3a
|
feat: clear%
|
2022-10-11 17:24:35 -07:00 |
|
Gabriel Ebner
|
7356840cbc
|
feat: use sepBy1Indent for tactic blocks
|
2022-09-18 16:43:23 -07:00 |
|
Sebastian Ullrich
|
a657a638f0
|
feat: sub-info tree level hover
|
2022-08-31 17:49:43 -07:00 |
|
Sebastian Ullrich
|
4050227e5d
|
chore: revert marking internal notes as parser/elab docstrings
|
2022-08-31 17:49:43 -07:00 |
|
Gabriel Ebner
|
82e9f09bca
|
fix: remove incorrect syntax coercion
|
2022-08-25 17:54:26 +02:00 |
|
Mario Carneiro
|
014db5d6d0
|
doc: relocate doc strings from elab to syntax
|
2022-08-13 17:16:40 -07:00 |
|
Mario Carneiro
|
b0db7deeef
|
doc: documentation for Init.Coe
|
2022-08-13 17:15:49 -07:00 |
|
Mario Carneiro
|
e816424466
|
chore: use Category declarations for builtin cats too (#1400)
|
2022-08-03 18:10:54 -07:00 |
|
Leonardo de Moura
|
e39eebabd9
|
fix: move doc string to parser that sets the SyntaxNodeKind for the { tac } notation
see #1403
This fixes the hover for `{ tac }`
|
2022-08-01 13:01:37 -07:00 |
|
Leonardo de Moura
|
2f00d60115
|
feat: helper parser for issue #1371
|
2022-07-31 04:30:02 -07:00 |
|
Mario Carneiro
|
9a401c852c
|
feat: add decl_name% / with_decl_name% macros
|
2022-07-29 21:42:51 +02:00 |
|
Leonardo de Moura
|
1bf53e4fc9
|
doc: add doc strings for let parsers
|
2022-07-27 10:56:44 -07:00 |
|
Mario Carneiro
|
f6211b1a74
|
chore: convert doc/mod comments from /- to /--//-! (#1354)
|
2022-07-22 12:05:31 -07:00 |
|
Leonardo de Moura
|
fd371ea812
|
chore: remove getOp builtin support
|
2022-07-09 16:04:17 -07:00 |
|
Sebastian Ullrich
|
d7bcc271be
|
refactor: avoid nested sequence in simpleBinder
|
2022-07-08 19:06:10 +02:00 |
|
Leonardo de Moura
|
131e7be8c5
|
feat: add a[i]? and a[i]! parsers
|
2022-07-02 07:29:58 -07:00 |
|
Sebastian Ullrich
|
f90e4ae30c
|
feat: more TSyntax API & coercions
|
2022-06-27 22:37:02 +02:00 |
|
Sebastian Ullrich
|
c202a2c013
|
feat: more antiquotation kinds
|
2022-06-27 22:37:02 +02:00 |
|
Sebastian Ullrich
|
2c54a0d17a
|
feat: allow anonymous antiquotations for tacticSeq
|
2022-06-27 22:37:02 +02:00 |
|
Sebastian Ullrich
|
3b3961a89b
|
chore: disable some anonymous antiquotations
|
2022-06-27 22:37:02 +02:00 |
|
Sebastian Ullrich
|
292d24ba19
|
feat: always store quoted kind in antiquotation kind
|
2022-06-27 22:37:02 +02:00 |
|
Gabriel Ebner
|
ec4200fc75
|
chore: remove unnecessary ppLine
|
2022-06-24 10:59:55 +02:00 |
|
Sebastian Ullrich
|
4212cc740b
|
refactor: move linebreak check into sepBy(1)Indent
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
|
2022-06-16 23:33:57 +02:00 |
|
Sebastian Ullrich
|
ce054fb2e7
|
fix: introduce semicolonOrLinebreak, replace many(1) with sepBy(1) where appropriate
|
2022-06-16 23:33:57 +02:00 |
|
Sebastian Ullrich
|
392640d292
|
feat: allow keyword-like projection identifiers
|
2022-05-10 12:25:30 -07:00 |
|
Leonardo de Moura
|
8d9626dab7
|
feat: delaborate match h : d with ...
|
2022-04-29 07:17:46 -07:00 |
|
Sebastian Ullrich
|
3cf2afa42e
|
refactor: clean up parsers using withAnonymousAntiquot := false
|
2022-04-06 10:21:53 +02:00 |
|
Sebastian Ullrich
|
ffee6676ef
|
feat: allow adjusting anonymous antiquot generation at leading_parser
|
2022-04-06 10:21:53 +02:00 |
|
Leonardo de Moura
|
eae4b92b0d
|
feat: use sorry if failed to synthesize default element for unsafe constant
|
2022-04-05 16:52:54 -07:00 |
|
Leonardo de Moura
|
8f4d58893f
|
feat: update match parser
Support for
```
def fib (x : Nat) : Nat :=
match x with
| 0 | 1 => 1
| x+2 => fib (x+1) + fib x
```
TODO: expand `matchAlts`
|
2022-03-20 13:22:39 -07:00 |
|
Leonardo de Moura
|
1c99fe92ac
|
feat: add dotIdent parser
see #944
|
2022-03-10 16:04:41 -08:00 |
|
Leonardo de Moura
|
5d2420b1c9
|
chore: add auxiliary notation for ForIn'
|
2022-03-03 19:10:24 -08:00 |
|
Leonardo de Moura
|
c67ee9fdf4
|
feat: add pp annotation for match parser
|
2022-02-14 15:46:52 -08:00 |
|
Leonardo de Moura
|
42c80c7483
|
feat: remove whitespace sensitivity at match discriminants
|
2022-02-14 15:37:40 -08:00 |
|
Leonardo de Moura
|
93b5b74b36
|
feat: modify notation for providing motive in "match" expressions
|
2022-02-14 15:36:14 -08:00 |
|
Leonardo de Moura
|
2c690926cf
|
feat: update namedPattern parser
|
2022-01-17 16:49:20 -08:00 |
|
Leonardo de Moura
|
bac91b9b5b
|
chore: remove arbitrary
|
2022-01-15 12:14:27 -08:00 |
|
Leonardo de Moura
|
9de58c66eb
|
chore: add default_or_ofNonempty%
|
2022-01-15 11:50:39 -08:00 |
|
Leonardo de Moura
|
0a726a755f
|
feat: add helper parser arbitrary_or_ofNonempty%
|
2022-01-14 17:11:55 -08:00 |
|
Mario Carneiro
|
5a7c9f2d35
|
chore: add showRhs definition
|
2022-01-04 09:28:29 -08:00 |
|
Mario Carneiro
|
9ee0d08cb5
|
chore: add doc
|
2022-01-04 09:26:34 -08:00 |
|
Mario Carneiro
|
3716e9a2ed
|
chore: use a different syntax kind for suffices-by
chore: update src/Lean/Parser/Term.lean
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
|
2022-01-04 09:26:32 -08:00 |
|
Gabriel Ebner
|
72851652f1
|
fix: spacing in suffices...by
|
2021-12-23 13:56:22 +01:00 |
|