Leonardo de Moura
ab31f9ad5d
fix: fixes #1143
2022-05-07 15:27:34 -07:00
Leonardo de Moura
3cf425ba52
fix: pattern hover information
...
We annotate patterns with the corresponding `Syntax` during
elaboration, and do not populate the info tree. Reason: the set of
pattern variables is not known during pattern elaboration.
2022-04-08 15:03:42 -07:00
Leonardo de Moura
4793c7e734
feat: add isAppOfArity variant that skips Expr.mdata
2022-04-08 15:01:57 -07:00
Leonardo de Moura
152eff5cea
chore: missing double ticks
2022-04-08 15:01:57 -07:00
E.W.Ayers
24ebd78071
doc: Expr.lean
2022-03-24 14:52:09 -07:00
Leonardo de Moura
e44b36cab0
chore: cleanup optimization using Lean bitwise operators
2022-03-15 12:06:08 -07:00
Leonardo de Moura
d3e2dfb079
perf: optimize mkApp
2022-03-15 11:31:15 -07:00
Leonardo de Moura
9d73317d76
perf: faster Expr.data
2022-03-15 11:30:41 -07:00
Leonardo de Moura
5283007aa4
feat: add HasConstCache
2022-03-15 08:39:48 -07:00
Leonardo de Moura
4e261b15e5
fix: smart unfolding bug in over applications
2022-03-14 19:17:21 -07:00
Leonardo de Moura
33883e9d2a
fix: resulting type of projection functions should not include auxiliary type annotations (e.g., autoParam)
2022-03-10 07:47:38 -08:00
Leonardo de Moura
5825eb394f
refactor: move isOutParam to Expr.lean, rename consumeAutoOptParam => consumeTypeAnnotations
2022-03-10 07:37:41 -08:00
Leonardo de Moura
164f07a5e5
feat: generalize Expr.abstractRange
...
It now takes free variables **and** metavariables.
This is the first step to make `mkForallFVars` and `mkLambdaFVars`
more general.
2022-03-08 18:19:17 -08:00
Leonardo de Moura
e574c5373f
feat: improve delta? method
...
Use zeta reduction to create new opportunities of beta-reduction.
This issue fixes on the problems that were affecting the generation of
equation theorems for `Array.heapSort.loop` (see issue: #998 ).
After this fix, the equation theorem generation fails at `splitMatch`.
2022-02-09 13:31:55 -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
Leonardo de Moura
763a337c25
chore: helper functions
2022-01-22 09:30:57 -08:00
Leonardo de Moura
0615020cf7
feat: make sure Expr.approxDepth does not overflow
2022-01-22 07:45:19 -08:00
Leonardo de Moura
b0083e0dd0
feat: use elaborated type to generate instance name
...
closes #951
2022-01-20 17:09:55 -08:00
Leonardo de Moura
b1a92f5cbf
feat: better Repr instances for Level.Data and Expr.Data
...
see #619
2022-01-20 09:45:30 -08:00
Leonardo de Moura
ff4be1e1db
feat: add Repr instances for Level and Expr
...
closes #619
TODO: a better `Repr` instance for `Expr.Data`
2022-01-20 09:26:06 -08:00
Leonardo de Moura
d782a97f5c
feat: add WF.mkProof for WF.mkEqns
2022-01-04 17:00:54 -08:00
Leonardo de Moura
58430704e5
refactor: move inaccessible? to Expr.lean
2021-10-20 15:54:18 -07:00
Leonardo de Moura
db5df69db4
fix: bounds check
...
fixes #704
2021-09-30 07:55:10 -07:00
Leonardo de Moura
c53d892f22
feat: add Expr.projExpr!
2021-09-27 19:06:10 -07:00
Leonardo de Moura
f40a9b7912
feat: add consumeAutoOptParam
2021-09-14 16:09:46 -07:00
Leonardo de Moura
1fd3cfb19f
feat: pretty print let_fun
2021-09-11 05:15:11 -07:00
Leonardo de Moura
445cc3085f
refactor: avoid Name, MVarId, and FVarId confusion
2021-09-07 19:06:50 -07:00
Leonardo de Moura
1d68f38aa6
feat: use approxDepth to compute hash code
2021-09-06 07:36:41 -07:00
Leonardo de Moura
fa29428934
feat: use 8-bits to store the approximate depth on an expression
...
We are going to use this information to (try to) minimize the number
of hash collisions.
2021-09-06 07:26:51 -07:00
Leonardo de Moura
397774157f
feat: nested tactic support in conv mode
2021-09-02 19:12:05 -07:00
Leonardo de Moura
391366ef24
refactor: add annotation for displaying conv state
2021-09-02 15:52:11 -07:00
Leonardo de Moura
fcbd807c9d
chore: some Expr constructors
2021-08-16 13:58:48 -07:00
Leonardo de Moura
5ef72057e9
feat: save additional information at StructureFieldInfo
2021-08-09 19:01:08 -07:00
Leonardo de Moura
d1d7ce1839
feat: start support for strict implicit binder annotation
2021-08-03 18:42:15 -07:00
Leonardo de Moura
635bc78d72
feat: use structure extension to implement Structure.lean
2021-08-02 18:03:20 -07:00
Leonardo de Moura
bba9353619
fix: make sure isDefEqOffset does not expose kernel nat literals
...
This issue is similar to a bug where `isDefEqOffset` was exposing
`Nat.add` when processing `HAdd.hAdd`.
Fixes #561
The example at issue #561 is now working, but we may have other places
where raw literals are being accidentally exposed.
2021-08-02 11:27:00 -07:00
Leonardo de Moura
ad216db08d
chore: add Repr instance for Literal and Key
2021-07-29 09:34:55 -07:00
Leonardo de Moura
7424f9c8b0
chore: remove HashableUSize
2021-06-02 09:58:46 -07:00
Leonardo de Moura
cbab9438c9
chore: Hashable instances for Expr and Level
2021-06-02 08:30:25 -07:00
Leonardo de Moura
43812444a7
chore: Hashable => HashableUSize
2021-06-02 07:24:26 -07:00
Leonardo de Moura
6a87bba9c0
chore: mixHash => mixUSizeHash
2021-06-02 07:05:42 -07:00
Leonardo de Moura
3a80e87793
chore: #405 step 1
2021-04-22 20:03:48 -07:00
Leonardo de Moura
f55561008c
fix: fixes #386
2021-04-11 20:57:39 -07:00
Leonardo de Moura
642342d6c1
feat: add Expr.eta
2021-04-09 14:21:21 -07:00
Sebastian Ullrich
e62542ed29
feat: CoeSort Bool Prop
2021-03-20 14:52:16 +01:00
Leonardo de Moura
865316bbf9
feat: improve error message when stuck solving universe constraints
...
closes #343
2021-03-11 17:46:44 -08:00
Leonardo de Moura
fc79b794ba
fix: missing error messages
...
Issue reported by @JasonGross
2021-03-05 17:20:04 -08:00
Leonardo de Moura
244b72befd
feat: simpArrow
2021-01-01 17:15:15 -08:00
Leonardo de Moura
5f6e66a53f
refactor: Repr
...
Modifications:
- Result type is `Format`
- It takes the context precedence like Haskell `Show`
2020-12-18 11:21:30 -08:00
Leonardo de Moura
0d9694d836
chore: user deriving BEq
2020-12-13 16:30:07 -08:00
