Leonardo de Moura
6af1da450e
feat: disable only eta for classes during TC resolution
...
closes #1123
2022-04-26 08:20:39 -07:00
Leonardo de Moura
6bc5433b17
fix: add support for heterogeneous equality at processGenDiseq
2022-04-25 16:56:03 -07:00
Leonardo de Moura
0c8a6d8977
feat: exists es:term,+ tactic
...
cc: @fgdorais
2022-04-25 15:35:31 -07:00
Leonardo de Moura
29b340aa36
fix: consume Expr.mdata at congr tactic
...
fixes #1118
2022-04-25 06:33:32 -07:00
Leonardo de Moura
3ad8dcb7ff
fix: nasty interaction between TC resolution and Eta for structures
...
See
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60constructor.60.20and.20.60Applicative.60/near/279984801
2022-04-24 08:19:29 -07:00
Leonardo de Moura
47b379e1bc
feat: dsimp! tactic
2022-04-23 18:41:04 -07:00
Leonardo de Moura
342a26a023
feat: dsimp tactic
2022-04-23 18:05:18 -07:00
Leonardo de Moura
13bcbe91cd
fix: regression reported at issue #1113
...
see issue #1113
2022-04-23 15:39:04 -07:00
Leonardo de Moura
34c75fc443
feat: allow ▸ even if the expected type is not available
...
see issue #1116
2022-04-23 08:00:27 -07:00
Leonardo de Moura
a82abee1b2
feat: sum of monomials normal form by reflection
2022-04-22 18:51:48 -07:00
Leonardo de Moura
875bf9bf34
fix: apply dsimp at lambda binders
...
This fixes another regression reported at #1113
2022-04-22 13:10:21 -07:00
Leonardo de Moura
c13ed7c0de
fix: regression reported at #1113
...
See #1113
2022-04-22 11:43:58 -07:00
Leonardo de Moura
66c82dadc9
fix: the default value for structure fields may now depend on the structure parameters
2022-04-21 17:38:19 -07:00
Leonardo de Moura
d1f10a2e71
feat: apply rfl theorems at dsimp
...
closes #1113
2022-04-21 16:26:57 -07:00
Leonardo de Moura
73076b855c
fix: bug at processGenDiseq
2022-04-20 10:46:05 -07:00
Leonardo de Moura
4848ad4869
feat: implement autoUnfold at simp
...
Right now, it only supports the following kind of definitions
- Recursive definitions that support smart unfolding.
- Non-recursive definitions where the body is a match-expression. This
kind of definition is only unfolded if the match can be reduced.
2022-04-18 16:51:52 -07:00
Leonardo de Moura
bb2df569bc
fix: bug at declare_config_elab
2022-04-18 14:56:22 -07:00
Leonardo de Moura
e6aee1e463
feat: make sure cases and induction alternatives are processed using the order provided by the user
...
Motivation: improve the effectiveness of the `save` and `checkpoint` tactics.
2022-04-18 11:45:36 -07:00
Leonardo de Moura
bc7f4fd02b
test: hasCSimpAttribute
2022-04-15 09:55:10 -07:00
Leonardo de Moura
4aee759ded
fix: make sure rfl is an extensible tactic
...
closes #1109
2022-04-15 08:51:05 -07:00
Leonardo de Moura
efb859013e
chore: ignore {} annotations at mk_projections
2022-04-13 10:16:41 -07:00
Leonardo de Moura
bd35e8a2be
chore: remove {} from ctor parser
2022-04-13 08:47:21 -07:00
Leonardo de Moura
3e0a975e9c
chore: fix test
2022-04-13 08:37:34 -07:00
Leonardo de Moura
dbf5366704
feat: ignore {} annotation at constructors
2022-04-13 08:30:21 -07:00
Leonardo de Moura
3bdb385c19
fix: make sure "eta for structures" in the elaborator uses projection functions if available
2022-04-11 19:23:10 -07:00
Leonardo de Moura
9f8dd99ccd
fix: macro declare_config_elab was corrupting the info tree
2022-04-11 16:49:56 -07:00
Leonardo de Moura
c2c2783f32
feat: improve dot name resolution by lazily unfolding resulting type
...
See new test to understand issue being fixed by this commit.
2022-04-10 14:37:27 -07:00
Leonardo de Moura
348037abbf
chore: move states35 to bench directory
...
@Kha It breaks in the CI in debug mode (stack overflow).
I think we have a mechanism for skipping some tests in debug mode, but
I forgot how it works.
2022-04-09 15:46:28 -07:00
Leonardo de Moura
1db11ed5c7
test: native_decide with 35 states
2022-04-09 14:48:53 -07:00
Leonardo de Moura
86bd70ac62
test: native_decide
2022-04-09 14:41:22 -07:00
Leonardo de Moura
7d99f6f555
perf: isClassQuick? was incorrectly producing undef
...
Then `isClassExpensive?` was being invoked too often. In some
benchmarks the performance hit was substantial. For example,
in the new test `state8.lean`. The runtime on my machine went from 2s
to 0.76s.
2022-04-09 10:38:49 -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
55989c25fc
chore: remove unnecessary args
2022-04-07 18:19:15 -07:00
Leonardo de Moura
d380808930
fix: generalize if target is a let-declaration
2022-04-06 11:08:41 -07: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
d7abecd07d
test: addDecorations without partial
2022-04-02 19:08:21 -07:00
Leonardo de Moura
c873ad6ef3
test: recursive function on Syntax without partial
2022-04-02 18:43:45 -07:00
Leonardo de Moura
9d55d7bf9e
feat: add helper tactic for applying List.sizeOf_lt_of_mem in termination proofs
2022-04-02 18:38:55 -07:00
Leonardo de Moura
64cfbc1ae3
feat: add helper tactic for applying sizeOf (a.get i) < sizeOf a automatically in termination proofs
2022-04-02 18:29:41 -07:00
Leonardo de Moura
03ec8cb30b
feat: missing sizeOf theorems for Array.get and List.get
2022-04-02 16:04:46 -07:00
Leonardo de Moura
a926cd1698
fix: mkUnfoldProof
...
The hypotheses in an equation theorem may depend on each other
2022-04-01 15:47:24 -07:00
Leonardo de Moura
4a0f68de83
fix: split tactic issue
2022-04-01 15:47:24 -07:00
Leonardo de Moura
0241d7c197
chore: fix tests
2022-04-01 11:34:50 -07:00
Leonardo de Moura
414f5596a6
test: Nat.binrec example
2022-04-01 08:29:44 -07:00
E.W.Ayers
4c2fedae50
doc: fix @Kha's issues with MonadControl
2022-04-01 10:06:58 +02:00
Leonardo de Moura
096e4eb6d0
fix: equation generation for nested recursive definitions
...
The issue was raised on Zulip. The issue is triggered in
declarations containing overlapping patterns and nested recursive
definitions occurring as the discriminant of `match`-expressions.
Recall that Lean 4 generates conditional equations for declarations
containing overlapping patterns.
To address the issue we had to "fold" `WellFounded.fix` applications
back as recursive applications of the functions being defined.
The new test exposes the issue.
2022-03-31 17:04:06 -07:00
Leonardo de Moura
6652d2665d
chore: remove old comment
2022-03-31 15:59:31 -07:00
Leonardo de Moura
734902bd3c
test: add split list example from Zulip without sorrys
2022-03-31 13:03:58 -07:00
Leonardo de Moura
2bd04285f8
fix : #1087
...
This commit is using the easy fix described at issue #1087 .
Hopefully the performance overhead is small.
closes #1087
2022-03-30 18:48:02 -07:00
Leonardo de Moura
63b9060ce9
chore: fix comments
2022-03-30 16:23:06 -07:00
