Mario Carneiro
|
8dfae9eb38
|
feat: import command stub
|
2022-10-12 11:11:31 -07:00 |
|
Gabriel Ebner
|
59abb9a332
|
feat: move docstring before | in ctors
|
2022-09-14 08:26:17 -07:00 |
|
Gabriel Ebner
|
54e7d31d0f
|
feat: allow empty whereStructInst
|
2022-09-13 06:19:40 -07:00 |
|
Mario Carneiro
|
3bb3efdedc
|
feat: allow optional type in example
|
2022-09-13 03:11:04 -07:00 |
|
Sebastian Ullrich
|
4050227e5d
|
chore: revert marking internal notes as parser/elab docstrings
|
2022-08-31 17:49:43 -07:00 |
|
Mario Carneiro
|
014db5d6d0
|
doc: relocate doc strings from elab to syntax
|
2022-08-13 17:16:40 -07:00 |
|
Sebastian Ullrich
|
d7e14ba47f
|
feat: openDecl antiquotation
|
2022-08-07 15:11:07 +02:00 |
|
Leonardo de Moura
|
55bb8e905a
|
chore: binderIdent normalization
fixes #1411
|
2022-08-04 21:10:02 -07:00 |
|
Mario Carneiro
|
25aea1b723
|
doc: document all the tactics
|
2022-08-01 08:08:03 -07:00 |
|
Leonardo de Moura
|
ab6af0118c
|
doc: add inductive command doc string
|
2022-07-30 15:15:16 -07:00 |
|
Sebastian Ullrich
|
a2ccf8f122
|
feat: accept keywords as constructor names
|
2022-07-28 12:46:28 -07:00 |
|
Leonardo de Moura
|
2c0de29dfd
|
feat: add add_decl_doc command
|
2022-07-27 09:30:32 -07:00 |
|
Mario Carneiro
|
f6211b1a74
|
chore: convert doc/mod comments from /- to /--//-! (#1354)
|
2022-07-22 12:05:31 -07:00 |
|
Sebastian Ullrich
|
8e07e80f72
|
feat: docComment parser alias
|
2022-07-22 14:30:49 +02:00 |
|
Sebastian Ullrich
|
cdb855d281
|
feat: support all sensible modifiers on (builtin_)initialize
Resolves #1324
|
2022-07-20 22:12:20 +02:00 |
|
Gabriel Ebner
|
243439a75c
|
feat: support modifiers in computed fields
|
2022-07-11 12:26:53 -07:00 |
|
Gabriel Ebner
|
b1eb022027
|
feat: computed fields
|
2022-07-11 12:26:53 -07:00 |
|
Sebastian Ullrich
|
d7bcc271be
|
refactor: avoid nested sequence in simpleBinder
|
2022-07-08 19:06:10 +02:00 |
|
Sebastian Ullrich
|
c64ac02ffc
|
fix: declModifiers syntax kind
|
2022-06-28 22:35:13 +02:00 |
|
Sebastian Ullrich
|
c202a2c013
|
feat: more antiquotation kinds
|
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 |
|
Leonardo de Moura
|
22c8f10b12
|
chore: remove constant command
|
2022-06-14 17:14:28 -07:00 |
|
Leonardo de Moura
|
05778565ab
|
feat: add opaque command
It will replace the `constant` command. See
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/What.20is.20.60opaque.60.3F/near/284926171
|
2022-06-14 16:22:36 -07:00 |
|
Leonardo de Moura
|
1e59eb2290
|
chore: update whereStructInst
|
2022-06-07 18:41:43 -07:00 |
|
Sebastian Ullrich
|
a2baf2cb96
|
refactor: split term/command quotations
|
2022-04-15 08:50:46 -07:00 |
|
Leonardo de Moura
|
8d2d0b3fbe
|
chore: remove {} from structure command
|
2022-04-13 10:19:00 -07:00 |
|
Leonardo de Moura
|
bd35e8a2be
|
chore: remove {} from ctor parser
|
2022-04-13 08:47:21 -07:00 |
|
Leonardo de Moura
|
addcbc6fa3
|
feat: process termination_by syntax
|
2022-01-12 16:15:30 -08:00 |
|
Leonardo de Moura
|
a1ab5c0ccb
|
feat: simplify termination_by new syntax
We don't need `using` anymore since we are going to use TC inference.
|
2022-01-12 08:28:03 -08:00 |
|
Leonardo de Moura
|
f9b79092f6
|
feat: new termination_by syntax
|
2022-01-11 15:36:50 -08:00 |
|
Leonardo de Moura
|
ce76ad44ea
|
feat: add terminationByCore parser
|
2022-01-11 14:44:36 -08:00 |
|
Gabriel Ebner
|
ab3e08190b
|
feat: allow opt-out of grouping in formatter
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
f1fc8f2441
|
fix: space before where/:= in inductive
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
3f73442a5a
|
fix: space before infer modifiers
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
b176efefca
|
fix: print line before deriving
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
52b36cad1d
|
fix: whitespace around parens in open/export
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
f219188c95
|
fix: indent declaration signatures
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
e90bdd00db
|
fix: indent where definitions and add space before
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
f5a2562575
|
fix: indent structure fields
|
2021-12-15 11:42:38 +00:00 |
|
Leonardo de Moura
|
55db56f80d
|
feat: add noncomputable section parser
|
2021-12-13 10:35:16 -08:00 |
|
Leonardo de Moura
|
bf3b0c53ad
|
chore: add helper parser
|
2021-12-12 08:16:42 -08:00 |
|
Leonardo de Moura
|
b6ef65d8fd
|
fix: where structure instance parser
closes #753
|
2021-12-12 07:52:52 -08:00 |
|
Scott Morrison
|
43315f7f94
|
fix: correct spacing in the pretty printer
|
2021-11-23 09:13:31 +01:00 |
|
Leonardo de Moura
|
85c49cfeb3
|
feat: apply termination tactic provided by user
|
2021-10-03 18:47:52 -07:00 |
|
Leonardo de Moura
|
23740778d4
|
refactor: termination hints
|
2021-10-03 18:09:35 -07:00 |
|
Leonardo de Moura
|
d22a42358f
|
feat: add decreasing_tactic notation
|
2021-10-03 17:16:29 -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 |
|