Sebastian Ullrich
ebe1e6d181
chore: remove misleading default for ParserCache.tokenCache
2020-08-06 09:26:48 -07:00
Sebastian Ullrich
0e8ef0cb8c
chore: document Format fields
2020-08-06 09:26:48 -07:00
Sebastian Ullrich
0f7f49aa06
feat: dbgTraceVal
2020-08-06 09:26:48 -07:00
Sebastian Ullrich
6f7a557e5a
feat: add --root flag to set package root directory
2020-08-06 09:21:52 -07:00
Leonardo de Moura
e818368c96
refactor: move EqnCompiler to Meta folder
2020-08-06 09:10:01 -07:00
Leonardo de Moura
9084c4fafc
feat: add DepElim.lean
2020-08-05 16:03:33 -07:00
Leonardo de Moura
eb32fec77e
feat: add admit tactic
2020-08-05 15:33:49 -07:00
Leonardo de Moura
b64e44fc44
fix: allow kernel projections to be used in inductive families containing only one constructor
2020-08-05 12:56:04 -07:00
Leonardo de Moura
9ddac04b40
fix: support for literals when compiling noConfusion
2020-08-05 10:17:51 -07:00
Leonardo de Moura
b3dcd35661
fix: bugs at cases tactic
2020-08-05 09:44:26 -07:00
Leonardo de Moura
a70962854e
chore: mark TODO
2020-08-04 18:50:53 -07:00
Leonardo de Moura
6be71b337f
refactor: add prototype2.lean
2020-08-04 18:35:11 -07:00
Leonardo de Moura
1ef5d322d7
chore: hack metavariable case
...
@Kha This is a small hack to improve debugging when developing the
new frontend using the old pretty printer.
2020-08-04 16:42:48 -07:00
Leonardo de Moura
943446f1b3
fix: FVarSubst must be a mapping from FVarId to Expr
...
Reason: `subst` tactic must store the `x |-> e` when substituting `x`
with `e`.
2020-08-04 13:06:08 -07:00
Leonardo de Moura
8aa375ba3e
fix: bug at FVarSubst generation
2020-08-03 17:47:24 -07:00
Leonardo de Moura
e43b5e27a1
feat: add processComplete
2020-08-03 17:02:53 -07:00
Leonardo de Moura
447000a797
fix: >>= associativity
2020-08-03 14:00:19 -07:00
Leonardo de Moura
33d4732e58
fix: processVariable bug
2020-08-03 12:33:19 -07:00
Leonardo de Moura
d206d85fcd
fix: trace class name
2020-08-03 11:36:15 -07:00
Leonardo de Moura
ad53983e35
feat: add FVarSubst.domain
2020-08-03 11:35:58 -07:00
Leonardo de Moura
252ef7345f
fix: incorrect FVarSubst for subst tactic
2020-08-03 11:35:14 -07:00
Leonardo de Moura
9746f8ab25
feat: apply variable substitution to Alts
2020-08-03 10:12:10 -07:00
Leonardo de Moura
fe0d298657
fix: mkAuxDefinition was not correctly handling delayed metavar assignments
2020-07-31 15:38:38 -07:00
Leonardo de Moura
edb25946d7
fix: instantiate metavars
2020-07-31 14:56:07 -07:00
Leonardo de Moura
0e473ba840
feat: add throwOther
2020-07-31 14:34:51 -07:00
Leonardo de Moura
55ecbe0c28
feat: add whnfAll cache
2020-07-31 11:34:51 -07:00
Leonardo de Moura
b23e59d509
feat: allow #eval to update Environment
...
See new `MetaHasEval`.
cc @Kha
2020-07-30 16:48:31 -07:00
Leonardo de Moura
7b82e401d5
feat: add getUnusedLevelParam
2020-07-30 14:01:25 -07:00
Leonardo de Moura
30e5b390ab
feat: use MessageData at Meta.Exception.appBuilder
2020-07-30 13:28:06 -07:00
Leonardo de Moura
e22e900784
feat: change Meta.Exception.other constructor
2020-07-30 13:06:57 -07:00
Leonardo de Moura
98e9fc20d5
feat: add replaceFVar
2020-07-30 13:06:45 -07:00
Leonardo de Moura
1e1ac497da
feat: add Meta.mkListLit and Meta.mkArrayLit
2020-07-29 18:01:26 -07:00
Leonardo de Moura
3ad1ffdd63
feat: add withExistingLocalDecls
2020-07-29 18:01:26 -07:00
Sebastian Ullrich
59de534270
fix: actually link Formatter.lean...
2020-07-29 18:19:56 +02:00
Sebastian Ullrich
1ceadd9f3d
feat: add [formatter] attribute
2020-07-29 18:02:57 +02:00
Sebastian Ullrich
1fe192802b
fix: parenthesizer
2020-07-29 15:18:00 +02:00
Sebastian Ullrich
d23625324c
refactor: move Syntax.Traverser
2020-07-29 15:18:00 +02:00
Leonardo de Moura
e234b9c671
feat: elaborate #print command
...
Basic `#print` command for helping us to test new frontend
2020-07-28 16:24:16 -07:00
Leonardo de Moura
7ea9a8c316
feat: add #print command parser
2020-07-28 14:56:10 -07:00
Leonardo de Moura
06a767089c
fix: do not use `mkAppM id #[e]``
...
If `e` has type `forall {A : Type}, B`, ``mkAppM `id #[e]`` fails
since it will try to synthesize the implicit argument `A : Type`.
We can avoid this issue by using
1- ``mkAppOptM `id #[none, some e]``, or
2- `mkId e`
2020-07-27 15:24:06 -07:00
Leonardo de Moura
14ab8344b6
fix: elaborate default value for parent field using parent field type
2020-07-27 15:19:06 -07:00
Leonardo de Moura
52353539c1
fix: track NameGenerator at CommandElabM
...
@Kha This was a super nasty bug. We did not notice it before because
most commands invoke `liftTermElabM` at most once. This is not true for
the new `structure` command. The bug manifested itself while I was
testing the new command. However, the issue was due to accidental
reuse of fresh variable Ids :)
2020-07-27 14:31:43 -07:00
Leonardo de Moura
81d2754cd2
chore: add headBeta to avoid unnecessary applications introduced by metavariable management
2020-07-24 16:05:05 -07:00
Leonardo de Moura
732dfed8b5
fix: id marker for auxiliary _default declarations
...
The "marker" is used to delimit parameters and the actual default
value (see new test).
2020-07-24 15:59:45 -07:00
Leonardo de Moura
857013634d
fix: auxiliary _default declaration name for parent default field values set in substructures
2020-07-24 15:54:55 -07:00
Leonardo de Moura
fb5440a074
fix: new frontend does not eagerly simplify universe level expressions
...
Remark: even if we change the new frontend to simplify all universe
level expressions, we should not rely on this property in the kernel.
Reason: users may still create terms without this property.
Remark: this bug was preventing the kernel from accepting valid declarations.
2020-07-24 15:45:01 -07:00
Leonardo de Moura
9dc5ca66e2
chore: use headBeta on type
2020-07-24 15:34:19 -07:00
Leonardo de Moura
7f43d01703
fix: assertion violation
2020-07-24 14:54:20 -07:00
Leonardo de Moura
2442794cf1
fix: auxiliary _default declaration binder information
2020-07-24 12:12:23 -07:00
Leonardo de Moura
5175138885
fix: preserve binder information
2020-07-24 12:11:05 -07:00
