max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
27951 commits 1 branch 0 tags 5.3 GiB
Commit graph

6720 commits

Author SHA1 Message Date
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
40c8db7494 feat: improve argument type mismatch error position, and do not stop at application type mismatch errors 2022-04-25 16:30:40 -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
ed12b62e28 fix: InfoTree was missing information for (pseudo) match patterns such as x + 1. 
This kind of pattern has to be reduced to a constructor, and the
`PatternWithRef` information was being lost in the process.
 2022-04-23 12:08:59 -07:00
Sebastian Ullrich
eb7bf2b272 fix: show single final state after tactic combinator 2022-04-23 17:42:32 +02:00
Sebastian Ullrich
240c5e15e9 fix: show final goal state at end of tactic combinator 2022-04-23 17:15:32 +02: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
57c3114875 fix: simpAll and tests 
We need another `update stage0` to remove workaround at `AC.lean`
 2022-04-21 15:00:07 -07:00
Leonardo de Moura
f891c5724d feat: track rfl simp theorems 
See issue #1113

We need update stage0 before closing the issue.
 2022-04-21 13:42:04 -07:00
Leonardo de Moura
0b92195ec8 feat: refine auto bound implicit feature 2022-04-21 10:17:15 -07:00
Leonardo de Moura
4727fd6883 feat: do not hightlight auxiliary declarations used to compile recursive definitions as variables 
They are "morally" constants.
 2022-04-21 08:11:22 -07:00
Leonardo de Moura
73076b855c fix: bug at processGenDiseq 2022-04-20 10:46:05 -07:00
Leonardo de Moura
597313135a fix: index out of bounds at computeFixedIndexBitMask 
closes #1112
 2022-04-19 05:21:43 -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
822375aaff chore: ensure _ alternative is the last one in the cases and induction tactics 2022-04-18 11:18:03 -07:00
Leonardo de Moura
726b735c6d fix: using invalid name generator at ContextInfo.runMetaM 
Already used `MVarId`s were being "reused" potentially creating cyclic
metavar assignment. See issue #1031 for an example.

closes #1031
 2022-04-15 18:42:34 -07:00
Sebastian Ullrich
7797fa3e2d fix: fun (x ...) ... should not be treated as a pattern 2022-04-15 10:00:26 -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
Sebastian Ullrich
a2baf2cb96 refactor: split term/command quotations 2022-04-15 08:50:46 -07:00
Leonardo de Moura
bcb9c2c2a3 chore: fix test 2022-04-13 10:27:59 -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
f098b1c291 test: for regression from last year's course at KIT 2022-04-13 08:31:43 -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
e49179c807 fix: simp at local declaration should not create an auxiliary declaration when result is definitionally equal 2022-04-11 07:54:15 -07:00
Leonardo de Moura
fb64a4ccc0 fix: unfold should not create an auxiliary declaration when result is definitionally equal 
This commit fixes an issue reported on Zulip
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unfolding.20the.20type.20of.20a.20variable.20creates.20a.20new.20variable
 2022-04-11 07:54:15 -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
e4304ea1de fix: always save completion info at resolveName 
See new test.
 2022-04-10 08:00:03 -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
4d077214f9 feat: jump to definition for match pattern variables 2022-04-09 15:36:42 -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