Leonardo de Moura
64bcb71b7a
chore: fix test
2020-07-14 16:44:02 -07:00
Leonardo de Moura
48c6c7c871
feat: report unused universe parameters
2020-07-14 16:40:56 -07:00
Leonardo de Moura
d4ae4da222
feat: check given constructor resulting type
2020-07-13 16:22:49 -07:00
Leonardo de Moura
920343d36b
fix: unspecified constructor resulting type is not allowed inductive families
2020-07-13 16:22:49 -07:00
Leonardo de Moura
2744ae96bb
feat: check unsafe annotations in mutually inductive datatype declarations
2020-07-13 16:22:49 -07:00
Leonardo de Moura
77ad630c80
test: inductive command
2020-07-13 16:22:49 -07:00
Leonardo de Moura
d5f64f52a9
feat: add CtorView and modifier validation for inductive and constructors
2020-07-13 16:22:48 -07:00
Leonardo de Moura
83431dc88e
feat: elaborate protected
2020-07-13 16:22:48 -07:00
Leonardo de Moura
fb6dfa4af2
chore: fix test
2020-07-13 16:22:48 -07:00
Leonardo de Moura
667f2ed601
feat: resolve inductive and ctor names
2020-07-13 16:22:48 -07:00
Leonardo de Moura
18fce4f455
feat: add Expr.inferImplicit
2020-07-13 16:22:48 -07:00
Leonardo de Moura
cda11dea25
feat: check universe parameters in mutually recursive inductive declaration
2020-07-11 08:01:36 -07:00
Leonardo de Moura
e26ec036ba
feat: add instantiateForall
2020-07-11 08:01:36 -07:00
Sebastian Ullrich
fb02fbb867
fix: freeing Environments in tests
2020-07-10 07:42:26 -07:00
Sebastian Ullrich
c38f4fe837
feat: unsafe functions for freeing compacted regions
2020-07-10 07:42:26 -07:00
Leonardo de Moura
f559576994
feat: inductive datatype header validation
2020-07-09 15:34:25 -07:00
Leonardo de Moura
cbb14673ef
chore: move RBTree and RBMap to Std
2020-06-25 13:26:16 -07:00
Leonardo de Moura
1612097788
chore: move HashMap and HashSet to Std
2020-06-25 12:46:56 -07:00
Leonardo de Moura
657879fcaa
chore: fix tests
2020-06-25 11:58:49 -07:00
Sebastian Ullrich
81376d3902
feat: allow capturing expected type in elab
...
/cc @leodemoura
2020-06-25 14:58:45 +02:00
Leonardo de Moura
80bb6f174d
feat: expand elab command
...
cc @Kha
2020-06-24 20:16:56 -07:00
Leonardo de Moura
6f8dbb4506
chore: fix test
2020-06-17 21:32:31 -07:00
Leonardo de Moura
82780be144
chore: fix tests
2020-06-17 21:28:37 -07:00
Sebastian Ullrich
0f0f1407af
chore: fix test
2020-06-17 18:07:44 +02:00
Sebastian Ullrich
5a10ac8f80
chore: delete platform-specific test
2020-06-17 10:53:10 +02:00
Leonardo de Moura
c6e7ea8fd5
feat: add ParserDescr.parser constructor for embedding parser definitions into parser descriptions
2020-06-16 14:06:46 -07:00
Leonardo de Moura
f61e4ffbbd
chore: ParserDescr.parser ==> ParserDescr.cat
2020-06-16 13:40:16 -07:00
Sebastian Ullrich
cfd1900625
fix: #eval: redirect stdout/stderr
2020-06-16 12:06:53 +02:00
Simon Hudon
a64e78b90b
feat: add std streams
...
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
2020-06-16 12:06:53 +02:00
Leonardo de Moura
bc6dba89f3
chore: fix tests
2020-06-15 14:39:30 -07:00
Sebastian Ullrich
43caef0130
fix: parenthesizer
2020-06-13 11:13:37 +02:00
Leonardo de Moura
6f0192581a
feat: change precedence for fun and do parsing rules to maxPrec
...
Motivation: avoid `$`. See new test.
cc @Kha
2020-06-11 16:24:04 -07:00
Leonardo de Moura
f92166e913
chore: fix test
2020-06-10 16:43:44 -07:00
Leonardo de Moura
f838b80e03
fix: elaboration functions for parser! and tparser!
2020-06-10 16:42:42 -07:00
Leonardo de Moura
f0a9e54a69
chore: make sure leading and trailing parsers use the same kind of check
2020-06-10 13:41:10 -07:00
Leonardo de Moura
25c1986439
chore: fix tests
2020-06-09 14:11:34 -07:00
Leonardo de Moura
7fce8b5d1f
fix: notation command
...
@Kha Note that I had to write the weird pattern
```
match_syntax stx with
| `(notation:$prec $items* => $rhs) => expandNotationAux stx prec items rhs
| `(notation $noprec* $items* => $rhs) => expandNotationAux stx none items rhs
| _ => Macro.throwUnsupported
```
with the weird `$noprec*` to match the case where the optional
precedence is not provided. I realized this is not a bug, but
I guess most users will be puzzled by this behavior. If we had a kind
for `notationItem`, I would be able to write
```
`(notation $items:notationItems* => $rhs)
```
2020-06-09 14:11:34 -07:00
Leonardo de Moura
4250bc630e
chore: fix tests
2020-06-08 16:18:46 -07:00
Leonardo de Moura
2b58ecea60
chore: fix test
2020-06-08 16:13:52 -07:00
Leonardo de Moura
f46dcd7a13
chore: fix some tests
2020-06-08 16:12:06 -07:00
Leonardo de Moura
dd1aa2f271
chore: improve error message
...
cc @Kha
2020-06-08 16:12:05 -07:00
Leonardo de Moura
c6ea675cae
chore: fix test
...
@Kha The error message changed. Not sure the new one is expected. It
is due to the change in `trailingLoop`. We can discuss it in the next
meeting.
2020-06-08 16:12:05 -07:00
Leonardo de Moura
aa66fc376b
chore: fix test
2020-06-08 16:12:05 -07:00
Leonardo de Moura
b3a8d417b2
chore: fix test
2020-06-08 16:12:05 -07:00
Leonardo de Moura
62cf913d6a
fix: interaction between errToSorry and observing.
...
@Kha I implemented the solution 1 I described at Zulip.
I also tried to document the issue, and made sure test
`choiceMacroRules` fail if the bug is reintroduced.
2020-06-08 12:37:43 -07:00
Leonardo de Moura
947369b4ce
chore: Parenthesizer issues after removing sortApp
...
@Kha Could you please double check these modifications.
I added a no-op for `checkRbpLt`. It is used at the `Sort` and `Type`
parsers.
As I described in previous commits, the `checkRBPGreater` comment and
implementation were misleading. It was actually succeeding when the
rbp was less than or equal to the given parameter. So, it was renamed
to `checkRbpLe`. So, is the depArrow parenthesizer ok? I did not check.
I updated the PPRoundtrip.lean.expected.out to make sure the tests
succeed, but we should revise it if there is a problem with the
modifications at Parenthesizer.lean
2020-06-03 15:46:33 -07:00
Sebastian Ullrich
6614b4d6e3
fix: use exact instead of prefix token match when inheriting precedence
...
/cc @leodemoura :)
2020-05-28 14:14:52 +02:00
Leonardo de Moura
5dffa0093a
feat: retrieve implicit lbp from Environment at syntax command
...
@Kha It is not clear to me why I had to change the following line
```
-syntax term ">>>" term : foo
+syntax term:1 ">>>":1 term : foo
```
The test breaks without it.
2020-05-27 17:11:57 -07:00
Leonardo de Moura
17b6957f6c
chore: fix tests
2020-05-26 15:05:01 -07:00
Leonardo de Moura
9c0bd9dd41
chore: fix tests
2020-05-26 15:05:00 -07:00
