Leonardo de Moura
2c06ba577e
chore: fix test
2020-11-17 17:14:06 -08:00
Leonardo de Moura
7e533b4650
refactor: use Lists for Array reference implementation
...
Motivation: better reduction in the kernel.
cc @Kha
2020-11-17 17:05:53 -08:00
Leonardo de Moura
8751bbe2a8
fix: notation for non reserved symbols
2020-11-17 11:25:04 -08:00
Leonardo de Moura
1d93eefada
feat: add ! x notation for notFollowedBy(x) in the syntax command
2020-11-17 10:57:15 -08:00
Leonardo de Moura
da23b96b43
feat: improve error messages for syntax command
2020-11-17 10:33:53 -08:00
Leonardo de Moura
178b3e5b52
chore: remove workaround
2020-11-16 16:25:58 -08:00
Leonardo de Moura
57670b633a
feat: improve smart unfolding
2020-11-16 15:44:52 -08:00
Leonardo de Moura
c81dbeb53c
feat: improve smart unfolding
2020-11-15 17:34:37 -08:00
Leonardo de Moura
f1b88e1304
feat: add option for disabling smart unfolding and fix tests
2020-11-15 17:00:51 -08:00
Leonardo de Moura
bb06fbaa8a
test: smart unfolding
2020-11-15 16:36:22 -08:00
Leonardo de Moura
f5ba036d8f
chore: add support for reducing matchers
2020-11-15 15:07:53 -08:00
Leonardo de Moura
0bf703b17c
chore: remove misleading comment
...
It doesn't loop in Lean 4.
2020-11-14 18:07:19 -08:00
Leonardo de Moura
73dec1be45
test: add tests for Lean3 bugs
2020-11-14 18:04:22 -08:00
Leonardo de Moura
db5fe843de
chore: add expandInterpolatedStr helper function, rename msg! => m!
2020-11-14 13:52:52 -08:00
Leonardo de Moura
cc7d7422db
fix: UInt ctors/fields in generated code
2020-11-14 12:50:32 -08:00
Leonardo de Moura
17fb995348
feat: improve mkLevelMax'
2020-11-14 08:36:23 -08:00
Leonardo de Moura
053e09c5e6
chore: fix test
2020-11-14 08:16:47 -08:00
Leonardo de Moura
99fad9fc4d
feat: goodies for writing notation with binders
2020-11-14 07:32:44 -08:00
Sebastian Ullrich
9c6c568caf
fix: don't try to pretty-print underapplied matcher
...
Fixes #219
2020-11-14 13:19:21 +01:00
Leonardo de Moura
b0e8183663
fix: error position for unsolved goals at cases and induction tactics
2020-11-13 07:59:50 -08:00
Leonardo de Moura
d137ecf4e8
feat: improve addLValArg
...
@Kha the module as classes test is now working.
2020-11-12 18:59:59 -08:00
Leonardo de Moura
61dfe2b1db
fix: letDecl
...
use `simpleBinderWithoutType` at `declSig` and `optDeclSig`
2020-11-12 16:22:57 -08:00
Leonardo de Moura
fc6c8e0348
fix: beta reduce value at processAssignmentFOApprox
2020-11-12 14:46:28 -08:00
Leonardo de Moura
367432defc
fix: fixes #217
2020-11-12 14:36:47 -08:00
Leonardo de Moura
cae6aa95dc
feat: support simpleBinder at letDecl
2020-11-12 13:25:38 -08:00
Leonardo de Moura
bd76458210
feat: add support for nonReservedSymbol at syntax command
2020-11-12 07:32:18 -08:00
Leonardo de Moura
65dafaf07c
fix: stdlib and tests
...
We also declare a few macros for the syntax command.
2020-11-12 07:12:30 -08:00
Leonardo de Moura
d30e96bc7d
chore: fix tests
2020-11-11 19:09:23 -08:00
Leonardo de Moura
ab2ee0390d
chore: fix tests
2020-11-11 10:19:14 -08:00
Leonardo de Moura
dbf99a17b6
chore: define notation using infix commands
2020-11-11 08:26:12 -08:00
Leonardo de Moura
7daeb7fffd
chore: fix test
2020-11-11 07:18:49 -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
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
2daeb195b5
chore: use new names
2020-11-10 10:15:19 -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
Leonardo de Moura
7e8a7e6660
feat: elaborate fun/forall binder extensions
2020-11-09 19:00:40 -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
82d6dd2eb6
feat: improve Structural.lean
2020-11-09 13:23:25 -08:00
Leonardo de Moura
425f45a623
chore: fix test
2020-11-09 06:43:52 -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
ef3f8c8723
feat: add funext tactic macro
2020-11-08 07:30:24 -08:00
Leonardo de Moura
6c6595cd9b
feat: only allow variables declared with mut to be reassigned
2020-11-07 17:32:13 -08:00
Leonardo de Moura
1e30d0831d
feat: allow recursive application in the discriminant of a nested match
2020-11-07 17:32:12 -08:00
Leonardo de Moura
81d6e065e7
chore: adjust files and tests
2020-11-07 17:32:12 -08:00
Sebastian Ullrich
c1d75e21ea
fix: fix pretty printers for imported ParserDescrs
...
... by interpreting them (imported or not) on the fly instead of storing them in the environment
/cc @leodemoura
2020-11-07 17:05:07 +01:00
Leonardo de Moura
4583f4344a
fix: SyntaxNodeKind at elab and macro commands
2020-11-05 17:20:41 -08:00
Leonardo de Moura
a37e24af4a
test: _root_
...
cc @Kha
2020-11-05 15:39:22 -08:00
