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

711 commits

Author SHA1 Message Date
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
Gabriel Ebner
d5142ddeb8 chore: add sepByIndent.formatter 2022-06-24 10:59:55 +02:00
Gabriel Ebner
733f220ee3 feat: $[...]* antiquotations for sepByIndent 2022-06-24 10:59:55 +02:00
Leonardo de Moura
d56163bd0e refactor: resolveNamespace now return a List 2022-06-16 17:16:36 -07: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
b585b2251e fix: adapt to stricter grammar 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
02c4e548df feat: replace constant with opaque 2022-06-14 17:02:59 -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
e52a7bdf42 feat: let/if indentation in do blocks 
closes #1120
 2022-06-13 16:18:49 -07:00
Leonardo de Moura
1e59eb2290 chore: update whereStructInst 2022-06-07 18:41:43 -07:00
Leonardo de Moura
041827bed5 chore: unused variables 2022-06-07 17:54:10 -07:00
Sebastian Ullrich
ae7b895f7a refactor: unname some unused variables 2022-06-07 16:37:45 -07:00
Sebastian Ullrich
ec045bfbb8 feat: $_ antiquotation pattern 2022-06-04 13:57:04 +02:00
Sebastian Ullrich
0a39e9cbdc fix: dynamic quotations should use previous stage by default 
@leodemoura as discussed some time ago
 2022-05-25 09:46:10 +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
829c81d677 fix: skip antiquotations during parser recovery 2022-04-27 10:41:27 +02:00
Sebastian Ullrich
83f331b5e2 parseCommand: use do 2022-04-27 10:41:27 +02:00
Sebastian Ullrich
a2baf2cb96 refactor: split term/command quotations 2022-04-15 08:50:46 -07:00
Sebastian Ullrich
e1fbc04c3b chore: accept unregistered syntax kinds in stage 1 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
de2e2447d2 chore: style 2022-04-07 17:35:05 -07:00
Sebastian Ullrich
24697026e8 feat: always accept antiquotations, simplify quotDepth code 2022-04-06 19:43:07 +02:00
Sebastian Ullrich
e10e664cc1 chore: typos 2022-04-06 10:21:53 +02: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
fdd1cb5751 chore: remove workarounds for #1090 2022-04-01 11:28:17 -07:00
Leonardo de Moura
799c701f56 fix: inconsistency between syntax and kind names 
TODO: remove staging workarounds

see #1090
 2022-04-01 11:20:16 -07:00
Leonardo de Moura
68acfc7fb9 chore: prepare for #1090 2022-04-01 11:11:28 -07:00
Leonardo de Moura
09de67780f chore: prepare for #1090 2022-04-01 09:35:06 -07:00
Leonardo de Moura
3dd0c84c4d chore: enforce naming convetion for tactics 2022-03-30 16:19:05 -07:00
Leonardo de Moura
46ce3013d0 feat: cleanup local context before elaborating match alternatives RHS 2022-03-29 18:52:07 -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
3862e7867b refactor: make String.Pos opaque 
TODO: this refactoring exposed bugs in `FuzzyMatching` and `Lake`

closes #410
 2022-03-20 10:47:13 -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
92937b3aba feat: add for h : x in xs do ... notation 
The idea is to have `h : x \in xs`.
This commit just adds the parser.
 2022-03-03 18:27:40 -08:00
Sebastian Ullrich
c9713b1b69 fix: setExpectedFn 2022-03-02 16:28:53 +01: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
12e2a79170 chore: fix codebase after removing auto pure 2022-02-03 18:08:14 -08:00
Leonardo de Moura
5f74cd4968 feat: add let pat := val | elseCase do-notation 2022-02-03 15:55:03 -08:00
Sebastian Ullrich
ce58ded16f fix: syntax match of literals 
Fixes #801
 2022-01-29 08:40:03 -08:00
Leonardo de Moura
cf3b8d4eb4 chore: cleanup 
Make the code style more uniform.
We still have a lot of leftovers from the old frontend.
 2022-01-26 09:18:17 -08:00