Leonardo de Moura
7daeb7fffd
chore: fix test
2020-11-11 07:18:49 -08:00
Leonardo de Moura
f936fe306c
chore: fix annotation
2020-11-11 07:15:13 -08:00
Leonardo de Moura
bf7660ff5a
chore: avoid infix operators at Prelude.lean
...
We also fix the copyright date
2020-11-11 06:56:45 -08:00
Leonardo de Moura
4c80714b12
chore: do not use infix operators at Quotation.lean
...
Reason: macros need to be used before the notation is defined.
2020-11-11 06:56:45 -08:00
Leonardo de Moura
9c9d65e640
chore: move definitions needed by macros to Prelude.lean
2020-11-11 06:56:45 -08:00
Leonardo de Moura
ccf69ae69d
fix: missing file
2020-11-11 05:56:47 -08:00
Leonardo de Moura
22e6cc1c75
chore: update stage0
2020-11-10 18:48:58 -08:00
Leonardo de Moura
6ab0be952c
chore: merge src/Control files
...
Some of them were almost empty after the refactoring.
2020-11-10 18:47:23 -08:00
Leonardo de Moura
a8c791ecae
chore: remove dead files and functions
...
Remove obsolete combinators: `whenM`, `unlessM`, and `condM`
cc @Kha
2020-11-10 18:37:15 -08:00
Leonardo de Moura
30fb78d627
chore: update stage0
2020-11-10 18:11:10 -08:00
Leonardo de Moura
cca3bad0bb
feat: add Prelude.lean
...
`Prelude.lean` has no dependencies, and
at the end of `Prelude`, the `syntax` and `macro` commands are operational.
2020-11-10 18:08:18 -08:00
Leonardo de Moura
3412c06059
chore: fix tests
2020-11-10 15:45:33 -08:00
Leonardo de Moura
687efdf974
chore: update stage0
2020-11-10 15:41:52 -08:00
Leonardo de Moura
c665d5e20a
chore: cleanup
2020-11-10 15:40:00 -08:00
Leonardo de Moura
7f364feeb5
chore: add Classical.lean, Equivalence, and cleanup
2020-11-10 14:55:34 -08:00
Leonardo de Moura
7e51020685
chore: move SizeOf to its own file
2020-11-10 14:43:03 -08:00
Leonardo de Moura
6c9c9c3955
chore: remove tactic framework dependency
2020-11-10 14:32:58 -08:00
Leonardo de Moura
7c393a1b3f
chore: cleanup
2020-11-10 14:06:11 -08:00
Leonardo de Moura
6ae2525e8f
chore: new prelude experiment
2020-11-10 14:02:58 -08:00
Leonardo de Moura
043fa5e16f
chore: update stage0
2020-11-10 12:35:22 -08:00
Leonardo de Moura
bd5c668347
feat: add helper functions for new Prelude.lean
2020-11-10 12:34:40 -08:00
Leonardo de Moura
de15bab918
chore: update stage0
2020-11-10 12:00:19 -08:00
Leonardo de Moura
1c01bd59be
chore: add numBitsEq
2020-11-10 11:59:16 -08:00
Leonardo de Moura
2daeb195b5
chore: use new names
2020-11-10 10:15:19 -08:00
Leonardo de Moura
cf0f4c04ed
chore: update stage0
2020-11-10 10:12:21 -08:00
Leonardo de Moura
2ef9199c56
chore: prepare to rename "predicate-like" classes
2020-11-10 10:12:21 -08:00
Sebastian Ullrich
e4f53fd92d
chore: adjust list & array spacing
2020-11-10 10:11:24 -08:00
Sebastian Ullrich
ce9be52ffb
feat: pretty print lists and arrays
2020-11-10 10:11:24 -08:00
Sebastian Ullrich
3665e3b7b5
feat: pretty print match
...
Fixes #177
2020-11-10 10:11:24 -08:00
Sebastian Ullrich
3d9f97574b
refactor: use and improve mkAppStx
2020-11-10 10:11:24 -08:00
Leonardo de Moura
33251fe069
chore: update stage0
2020-11-09 19:01:46 -08:00
Leonardo de Moura
7e8a7e6660
feat: elaborate fun/forall binder extensions
2020-11-09 19:00:40 -08:00
Leonardo de Moura
faa9ea3c98
chore: update stage0
2020-11-09 18:45:35 -08:00
Leonardo de Moura
25083fba9f
feat: extend binder syntax
2020-11-09 18:41:48 -08:00
Leonardo de Moura
defa45ae2f
feat: improve error message
...
when match-expression LHSs still contain metavariables after elaboration
2020-11-09 18:26:14 -08:00
Leonardo de Moura
f91b2cc89c
chore: typo
2020-11-09 18:13:02 -08:00
Leonardo de Moura
82d6dd2eb6
feat: improve Structural.lean
2020-11-09 13:23:25 -08:00
Leonardo de Moura
c7ebc33f97
chore: fix typo
2020-11-09 11:43:57 -08:00
Leonardo de Moura
f1a2d4dee1
doc: fix and expand lean3changes.md
2020-11-09 11:37:34 -08:00
Leonardo de Moura
425f45a623
chore: fix test
2020-11-09 06:43:52 -08:00
Leonardo de Moura
cf77799364
doc: add lean3changes.md
2020-11-08 14:25:56 -08:00
Leonardo de Moura
fdb7db5650
chore: rename Eq.subst argument
2020-11-08 14:05:17 -08:00
Leonardo de Moura
ded043bd53
test: old Lean3 begin ... end as a macro
...
@Kha I am adding a few examples to use in the manual.
This one is a bit ugly due to two issues
1- We can't easily copy the position information from one token to
another. You suggested a notation in the past, but we never
implemented it. In the new example, we must copy the `end` position to
`}` to get the "unsolved goals" error message at the `end` token.
2- The quotation `` `(by { $ts* }) `` doesn't do what we want.
The issue is that we are using `group` instead of `nodeWithAntiquot`
to define `tacticSeqBracketed`. I will have to go over all parsers we
have defined, and check how many other places have this problem.
2020-11-08 11:53:13 -08:00
Leonardo de Moura
a8a457b355
refactor: move getTailInfo/copyTailInfo/etc to LeanInit
2020-11-08 11:52:14 -08:00
Leonardo de Moura
1f592ddf92
chore: update stage0
2020-11-08 08:13:59 -08:00
Leonardo de Moura
029510d4f5
feat: syntax for setting allowTrailingSep
...
@Kha This commit allows us to set `allowTrailingSep` for `sepBy` and
`sepBy1` from the `syntax` command.
```lean
syntax "[" (sepBy (allowTrailingSep := true) term ",") "]" : term
```
The new syntax is a bit verbose :)
What do you think? Any suggestions?
2020-11-08 08:12:54 -08:00
Leonardo de Moura
4a3b9c75e1
feat: add Quote Bool instance
2020-11-08 08:07:17 -08:00
Leonardo de Moura
fc4d991707
feat: add allowTrailingSep parameter to ParserDescr.sepBy and ParserDescr.sepBy1
2020-11-08 07:51:10 -08:00
Leonardo de Moura
ef3f8c8723
feat: add funext tactic macro
2020-11-08 07:30:24 -08:00
Leonardo de Moura
c03b98e46e
chore: update stage0
2020-11-08 07:24:20 -08:00
