Leonardo de Moura
c6dfecb7aa
feat: helper notation for controlling elaboration order
2021-10-02 15:10:27 -07:00
Leonardo de Moura
acd21052c0
chore: remove old notation
2021-10-02 15:06:40 -07:00
Leonardo de Moura
9337498c5b
chore: keywords should be snake_case
2021-10-02 14:54:48 -07:00
Leonardo de Moura
2bc24ff619
chore: let_zeta => let_tmp
2021-09-30 22:19:06 -07:00
Leonardo de Moura
b83facc738
feat: add let_zeta auxiliary parser
2021-09-30 22:08:11 -07:00
Leonardo de Moura
7c0993ae12
chore: add pp annotations to if parser
2021-09-30 20:40:02 -07:00
Leonardo de Moura
698760c5eb
refactor: add if-then-else builtin parser
2021-09-30 19:33:41 -07:00
Leonardo de Moura
200a38e20c
feat: improve letIdLhs parser
...
The extra space is only really needed to distinguish an array update (NIY)
```
let x[i] := ...
```
from a declaration taking an instance argument
```
let f [Monad m] := ...
```
closes #696
2021-09-28 18:10:25 -07:00
Leonardo de Moura
8425a53377
feat: improve termination_by notation
2021-09-22 21:08:01 -07:00
Leonardo de Moura
6211b95e06
feat: add termination_by parser
2021-09-21 13:19:01 -07:00
Sebastian Ullrich
585fba69e8
refactor: remove redundancy from common register_parser_alias case
...
/cc @leodemoura
2021-09-20 13:20:23 +02:00
Leonardo de Moura
f43ab76641
feat: doc string for syntax abbreviations
2021-09-12 18:26:36 -07:00
Leonardo de Moura
53ec43ff9b
refactor: lazy evaluation for >>, <*>, <*, and *>
...
see issue: #617
2021-09-07 17:50:34 -07:00
Leonardo de Moura
3714cf16ec
refactor: lazy evaluation for <|>
...
see #617
2021-09-07 17:06:10 -07:00
Leonardo de Moura
d991c20859
chore: add binop_lazy%
...
This is a gadget for issue #617 .
2021-09-07 13:00:36 -07:00
Leonardo de Moura
bbb74bfd9a
feat: elaborate optional deriving after def
2021-09-03 10:22:17 -07:00
Leonardo de Moura
8a268e184b
feat: update def parser with optional deriving ...
2021-09-03 09:42:17 -07:00
Leonardo de Moura
d7537f252a
chore: remove unnecessay parser/elab
2021-09-02 17:29:32 -07:00
Leonardo de Moura
6d8058034a
chore: basic conv mode parsers
2021-09-01 15:35:32 -07:00
Leonardo de Moura
d67c633ca1
feat: allow user to set "behavior" at declare_syntax_cat
2021-09-01 13:28:12 -07:00
Leonardo de Moura
56961060d4
fix: use rawIdent at eraseAttr parser
...
Reason: some attribute names are also keywords (e.g., `instance`).
2021-08-31 15:07:21 -07:00
Sebastian Ullrich
e632c14f3f
chore: align stx precedence in syntax to the new one in macro
2021-08-24 10:11:12 -07:00
Leonardo de Moura
79e6732fc6
fix: update tokenTable at withNamespace parser combinator
...
It also moves `withOpen` and `withOpenDecl` applications to simplify
their definitions and make sure we do not need to reset the cache.
2021-08-23 09:41:36 -07:00
Leonardo de Moura
7edc42fdfc
fix: scoped command after open command
...
The issue was reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Ending.20a.20command
2021-08-23 08:29:30 -07:00
Leonardo de Moura
d93c4317d1
feat: add withOpenDecl and withOpen parsers
...
It allow us to process `open .. in ..` while parsing.
This is useful for activating a scoped parser while parsing.
TODO: `openOnly` and `openHiding`, these two cases are rarely used
with `open .. in ..`
closes #529
2021-08-22 20:50:35 -07:00
Leonardo de Moura
54316fabb4
feat: add nonrec parser
2021-08-21 16:39:18 -07:00
Leonardo de Moura
519bb1e7d4
feat: add open scoped parser
2021-08-21 07:06:50 -07:00
Sebastian Ullrich
9c15f94be3
perf: do not use parsers from the current stage inside quotations by default
2021-08-12 07:51:50 -07:00
Sebastian Ullrich
20accf5105
feat: revise macro parameter syntax
2021-08-12 07:48:42 -07:00
Leonardo de Moura
09c2b668e6
feat: allow multiple sources in the structure instance parser
...
This commit also fixes some macros, and make sure the elaborator still
works, but it does not support multiple sources yet.
2021-08-11 13:07:56 -07:00
Leonardo de Moura
3293e9ef08
chore: fix module comments, they must occur after the imports
2021-08-06 14:02:42 -07:00
Leonardo de Moura
5796b93134
fix: support for /-! at whitespace
2021-08-06 13:52:32 -07:00
Leonardo de Moura
8d5964ce19
feat: add module doc parser
2021-08-06 13:17:56 -07:00
Leonardo de Moura
257e38394f
feat: add strict implicit binder annotation
2021-08-03 19:10:51 -07:00
Leonardo de Moura
c913886938
chore: add private annotations
2021-08-03 18:15:39 -07:00
Leonardo de Moura
f9672fe4c6
feat: add optional visibitily modifier to initialize and builtin_initialize commands
2021-08-03 14:37:22 -07:00
Daniel Selsam
6940166db4
chore: rebase and rm rawPos
2021-08-03 09:13:18 +02:00
Daniel Selsam
89364b802b
feat: top-down heuristic delaboration
2021-08-03 09:13:18 +02:00
Leonardo de Moura
bba9353619
fix: make sure isDefEqOffset does not expose kernel nat literals
...
This issue is similar to a bug where `isDefEqOffset` was exposing
`Nat.add` when processing `HAdd.hAdd`.
Fixes #561
The example at issue #561 is now working, but we may have other places
where raw literals are being accidentally exposed.
2021-08-02 11:27:00 -07:00
Sebastian Ullrich
32bea73708
fix: ensure hygiene of double-quoted names
...
Fixes #586
2021-07-30 07:17:50 -07:00
Leonardo de Moura
fb3ea8109f
fix: structure instance parser
2021-07-27 12:54:17 -07:00
Wojciech Nawrocki
cfb5d34dd3
fix: parser arity
2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
4a3c172ac9
feat: parametrised deriving handlers
2021-07-24 10:45:28 +02:00
Sebastian Ullrich
5866e2bbb7
chore: use register_parser_alias where possible
...
Fixes #494
2021-07-22 16:28:06 +02:00
Sebastian Ullrich
42e681a5a6
fix: make unterminated comments consume all input
...
Fixes #549
2021-07-22 15:55:12 +02:00
Sebastian Ullrich
8637220927
fix: make precedence mandatory for mixfix commands
...
Resolves #577
2021-07-19 13:18:58 -07:00
Wojciech Nawrocki
a8d599a955
fix: typo
2021-07-15 21:57:55 +02:00
Leonardo de Moura
f4a7ffd8c8
chore: fix codebase and tests
2021-06-29 17:14:52 -07:00
Leonardo de Moura
90a79a0b06
chore: remove command universes
...
Now, `universe` may declare many universes. The goal is to make it
consistent with the `variable` command
2021-06-29 17:01:07 -07:00
Sebastian Ullrich
3f4ab0a2af
feat: implement elab_rules
...
TODO: infer category from quotation type
2021-06-21 10:17:26 -07:00
