max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
21887 commits 1 branch 0 tags 5.3 GiB
Commit graph

96 commits

Author SHA1 Message Date
Leonardo de Moura
24d41b9518 chore: move to new frontend 2020-10-21 12:16:30 -07:00
Leonardo de Moura
a052446414 feat: simplify decide! and nativeDecide! macros 2020-10-20 15:08:16 -07:00
Leonardo de Moura
ef18b0ab49 chore: use [builtinInit] 2020-10-19 14:58:38 -07:00
Leonardo de Moura
60e4f4fee1 feat: improve notFollowedBy error messages 2020-10-15 17:01:10 -07:00
Sebastian Ullrich
78ffc72150 chore: remove ppGroups beneficial only for group but not fill 2020-10-14 14:24:47 +02:00
Leonardo de Moura
d2e5c1c300 feat: improve dbgTrace! macro 2020-10-13 12:38:04 -07:00
Leonardo de Moura
9538772c1c chore: do not use string interpolation by default at dbgTrace! 
It is nice to be able to write `dbgTrace! x` instead of `dbgTrace! "{x}"`
 2020-10-09 20:49:39 -07:00
Leonardo de Moura
bca81714fe feat: println! and dbgTrace! macros with string interpolation 2020-10-09 17:19:04 -07:00
Leonardo de Moura
e021a7d011 chore: remove symbolNoWs 
@Kha This is a leftover from the time precedence was associated with
tokens instead of parsers.
 2020-10-09 16:17:56 -07:00
Sebastian Ullrich
064c9b2e0b chore: binder spacing 2020-10-07 09:46:47 +02:00
Sebastian Ullrich
21f1a66ceb feat: add & use ppDedent parser combinator 2020-10-07 09:46:47 +02:00
Sebastian Ullrich
88164a5e91 feat: more pp tweaks 2020-10-07 09:44:05 +02:00
Sebastian Ullrich
5d76a981b0 chore: adjust pp spacing 2020-10-07 09:44:04 +02:00
Sebastian Ullrich
bdff53fdf5 feat: use ppLine 2020-10-07 09:43:05 +02:00
Leonardo de Moura
db5fdd15c4 feat: add let* parser and add some support for it at Binders.lean 2020-10-06 14:42:47 -07:00
Leonardo de Moura
ef2d9b4d59 feat: add ensureExpectedType! parser 2020-10-06 09:31:21 -07:00
Leonardo de Moura
10fc908463 chore: use Tactic.seq1 instead of Tactic.tacticSeq1Indented 
Reason: antiquotations.
 2020-10-06 08:28:41 -07:00
Leonardo de Moura
c3b0e9936c chore: group many elements 2020-10-06 08:28:40 -07:00
Leonardo de Moura
93dc94b3b0 chore: remove nodeSepBy1Unbox hack 2020-10-06 07:22:28 -07:00
Leonardo de Moura
7325dcd630 feat: use do at for-in and unless notations 2020-10-05 09:43:11 -07:00
Leonardo de Moura
6db45891e2 feat: add typeOf! and ensureTypeOf! parsers 2020-10-01 14:33:04 -07:00
Leonardo de Moura
4e72530ce7 chore: let rec in do blocks 2020-10-01 10:40:11 -07:00
Leonardo de Moura
0911b9bc80 feat: add missing features to do notation parser 2020-09-30 06:51:25 -07:00
Leonardo de Moura
e10edde5cd feat: optional ; in terms 2020-09-28 17:10:59 -07:00
Leonardo de Moura
d4c1432574 fix: tacticSeqBracketed 2020-09-28 17:10:59 -07:00
Leonardo de Moura
f45fa34cba feat: optional ; at tacticSeq1Indented 2020-09-28 17:10:59 -07:00
Leonardo de Moura
7f9013e496 fix: seq1Unbox 2020-09-28 17:10:59 -07:00
Leonardo de Moura
85d8c4fa85 chore: add proper kind for tacticSeq1Indented 2020-09-28 17:10:59 -07:00
Leonardo de Moura
aa410283c6 fix: we don't want antiquotation for seq1 2020-09-28 17:10:59 -07:00
Leonardo de Moura
cb55ffae94 chore: add new tactic syntax kind 2020-09-28 17:10:58 -07:00
Leonardo de Moura
861fd11a57 chore: add tacticSeq node 
We use `$tac:tacticSeq` in many places, and we want them to match
the bracketed and indented cases.
 2020-09-28 17:10:58 -07:00
Leonardo de Moura
6f211d3449 chore: adjust tactic parser 2020-09-28 17:10:57 -07:00
Leonardo de Moura
93090baa82 chore: cleanup tactic syntax 2020-09-28 17:10:57 -07:00
Leonardo de Moura
08d54b6043 feat: add checkColGt at app 
@Kha Only one example broke :)
 2020-09-28 17:10:57 -07:00
Leonardo de Moura
6ddec22763 refactor: simplify withPosition combinator 
Add `checkColGt`
 2020-09-28 17:10:56 -07:00
Leonardo de Moura
2d8506b7c6 feat: add doElem parser category 2020-09-26 06:18:44 -07:00
Leonardo de Moura
dc9626ceab feat: try to improve weird error message 
@Kha Before this commit, we were producing the error "expected command" at the `let` token
```lean
check id let x := 1; x
```
The new error is "expected command, but found term; this error may be
due to parsing precedence levels, consider parenthesizing the term".

The example above looks artificial, but it will happen all the time as
users start to define their own notation.
 2020-09-21 18:29:01 -07:00
Sebastian Ullrich
68568e78d3 feat: formatter: use hard space after opening structure instance brace 2020-09-18 13:15:40 -07:00
Sebastian Ullrich
95007171a8 feat: formatter: group+indent binders and structure instance fields 2020-09-18 13:15:40 -07:00
Leonardo de Moura
d1c3ab3797 feat: many1Unbox and nodeSepBy1Unbox parser combinators 
@Kha I removed the dummy parenthesizer/formatter for `withResultOf`,
and add proper ones for `many1Unbox` and `nodeSepBy1Unbox`.
 2020-09-17 13:17:46 -07:00
Leonardo de Moura
2dafdec000 feat: use withResultOf combinator instead of unboxSingleton parameter 2020-09-17 12:12:12 -07:00
Sebastian Ullrich
fad4660135 feat: pretty print space between binders 2020-09-17 08:12:28 -07:00
Leonardo de Moura
c49ccda46a feat: add antiquotation for indentedNonEmptySeq 2020-09-14 14:57:38 -07:00
Leonardo de Moura
05e6a779ba fix: can't use maxPrec at by 
If `by` uses `maxPrec`, then `have A by B ...` is parsed as
`have (A by B) ...` :(

cc @Kha
 2020-09-14 14:57:14 -07:00
Leonardo de Moura
f95675dc22 feat: add have-by and show-by syntax 2020-09-14 14:25:35 -07:00
Leonardo de Moura
fc4ab139b5 feat: indented by 
@Kha This one is not as useful as the indented `do`. When writing
interactive proofs I like the error message at the `}` showing the
resulting tactic state. We can simulate it using a `skip` in the end of the sequence :)
We remove the `skip` when the proof is done. Note that, the last `;`
is usually not part of the `by`. Example:
```lean
theorem ex (x y z : Nat) : y = z → y = x → x = z :=
fun _ _ =>
  have x = y by apply Eq.symm; assumption; -- <<< the last `;` is part of the `have`
  Eq.trans this (by assumption)
```
 2020-09-14 14:20:02 -07:00
Leonardo de Moura
4c6a589e6c feat: indented do blocks 
@Kha it is soooooo much nicer :)
 2020-09-14 13:44:51 -07:00
Leonardo de Moura
151012cb39 feat: remove emptyc elaboration hack 
@Kha I removed the hack. We know get a nice error message.
 2020-09-11 14:41:44 -07:00
Leonardo de Moura
ba4fdce508 feat: expand helper macros 2020-09-10 14:25:07 -07:00
Leonardo de Moura
d77dc5efb8 feat: add helper syntax 2020-09-10 13:31:45 -07:00