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

7361 commits

Author SHA1 Message Date
Leonardo de Moura
66e0b72c6f test: notation for providing names to equality proofs in match expressions is not whitespace sensitivity anymore 2022-02-14 15:51:23 -08:00
Leonardo de Moura
764a1d9f51 chore: fix tests 2022-02-14 15:47:12 -08:00
Leonardo de Moura
93b5b74b36 feat: modify notation for providing motive in "match" expressions 2022-02-14 15:36:14 -08:00
Leonardo de Moura
07043e73b0 chore: fix tests 2022-02-14 12:06:03 -08:00
Leonardo de Moura
aa63fda835 fix: mark auxiliary noConfusion declarations for enumeration types as [reducible] 
closes #1016
 2022-02-14 12:03:49 -08:00
Leonardo de Moura
82bce7ebec fix: declare local instaces occurring in patterns 2022-02-12 12:01:08 -08:00
Leonardo de Moura
999e80745e test: add test for already fixed issue reported on Zulip 2022-02-12 07:53:31 -08:00
Leonardo de Moura
ab41dd0d83 test: add test for issue #1013 2022-02-11 09:28:46 -08:00
Leonardo de Moura
123e0f42e9 feat: support partial and over applications at WF/PackDomain.lean 
closes #1013
 2022-02-11 09:28:17 -08:00
Sebastian Ullrich
80e2e1daa8 test: mutual block not needed 2022-02-11 16:22:13 +01:00
Leonardo de Moura
712d6726e4 feat: rename tactic byCases => by_cases 2022-02-10 17:11:07 -08:00
Sebastian Ullrich
894dc0e1b8 fix: pretty-printing match dependent on let 2022-02-10 10:19:04 +01:00
Leonardo de Moura
54473ad523 test: add missing test for issue #998 2022-02-09 18:02:01 -08:00
Leonardo de Moura
9fe0d28107 fix: do not split on if-then-else terms when generating equation theorems 
Reason: avoid unnecessary case-analysis explosion
It is also unnecessary since we only refine the `below` and `F`
arguments over `match`-expressions.

This fixes the last case at issue #998
```
attribute [simp] BinaryHeap.heapifyDown
```

closes #998
 2022-02-09 17:43:35 -08:00
Leonardo de Moura
7fc12014da fix: make sure splitTarget? skips match expressions that produce type errors at splitMatch 
We can now generate the equation theorem for
```
attribute [simp] Array.heapSort.loop
```

see #998
 2022-02-09 17:07:10 -08:00
Sebastian Ullrich
8cbd7ccf09 test: reimplement package tests using Lake 2022-02-09 12:21:11 -08:00
Leonardo de Moura
15e6dd262d chore: fix tests 2022-02-09 10:13:52 -08:00
Leonardo de Moura
3b67c7db81 fix: handling of letrec declarations in the well-founded recursion module 2022-02-09 10:13:52 -08:00
Sebastian Ullrich
9e11ea3b34 chore: move test to correct folder 2022-02-09 14:32:18 +01:00
Sebastian Ullrich
a8e34b9310 test: mutual recursion over mutual inductive 2022-02-09 14:24:45 +01:00
Leonardo de Moura
2ef0146140 fix: avoid unnecessary matcheApp.addArgs at BRecOn and Fix 
It fixes the following two cases from #998
```
attribute [simp] Lean.Export.exportName
attribute [simp] Lean.Export.exportLevel
```
 2022-02-08 15:06:14 -08:00
Leonardo de Moura
8692225432 fix: saveEqn at Lean/Elab/PreDefinition/Eqns.lean 
see #998
 2022-02-08 13:44:49 -08:00
Leonardo de Moura
afb5cb16ee chore: simplify option names 
see #1011
 2022-02-08 12:23:24 -08:00
Leonardo de Moura
59acf01bc9 feat: relax auto-implicit restrictions 
The new options `relaxedAutoBoundImplicitLocal` can be used to
disable this feature.

closes #1011
 2022-02-08 12:17:42 -08:00
Leonardo de Moura
398b9c136a chore: fix test 2022-02-08 11:43:45 -08:00
Leonardo de Moura
96336bb44d test: add tests for #998 
The previous changes fixed two of them.
 2022-02-08 11:43:45 -08:00
Leonardo de Moura
c486203481 fix: use simpTargetStar when proving equation theorems for recursive definitions 
Add `take` function reported at Zulip.
 2022-02-08 11:43:45 -08:00
Leonardo de Moura
8d7f0ea2f2 feat: add removeUnnecessaryCasts 
see #988
 2022-02-07 17:24:32 -08:00
Leonardo de Moura
9d34d9bc5a feat: cache and optimize mkCongrSimp? at simp 
see #988
 2022-02-07 17:01:21 -08:00
Leonardo de Moura
007f0e1d71 feat: use mkCongrSimp? at simp 
TODO: cache auto generated congr theorems, and `removeUnnecessaryCasts`

see #988
 2022-02-07 16:45:01 -08:00
Leonardo de Moura
5baac1905f fix: use private names for theorems that are created on demand 
closes #1006
 2022-02-07 13:16:22 -08:00
Leonardo de Moura
eff63632b3 feat: improve error message when max heartbeats is reached during TC 
see #1007
 2022-02-07 11:23:48 -08:00
Gabriel Ebner
f8b43630a6 fix: refs to copied subobjects in diamond extension 2022-02-07 10:54:32 -08:00
Leonardo de Moura
8cea32f42d chore: fix test 2022-02-06 09:15:39 -08:00
Sebastian Ullrich
2c7d67d498 fix: make info of fields synthesized by structure update synthetic 2022-02-06 08:50:07 -08:00
Sebastian Ullrich
0ef5985b5f fix: binder info range for let rec/where 2022-02-06 07:21:51 -08:00
Leonardo de Moura
6de0b1fc67 feat: add mkCongrSimp.mkProof 
see #988
 2022-02-04 17:57:28 -08:00
Leonardo de Moura
3ae455bccf feat: add mkCongrSimp? 
TODO: proof is still missing

see #988
 2022-02-04 17:57:28 -08:00
Leonardo de Moura
a028a69159 feat: cache isProp and isDecInst at FunInfo 2022-02-04 17:57:28 -08:00
Sebastian Ullrich
a7ba103e0a chore: remove leanpkg 2022-02-04 19:03:40 +01:00
Sebastian Ullrich
ae062c6ead fix: match tactic should not trigger implicit lambdas 2022-02-04 07:55:56 -08:00
Leonardo de Moura
e9d85f49e6 chore: remove tryPureCoe? 
Based on the discussion at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/for.2C.20unexpected.20need.20for.20type.20ascription/near/269083574
The consensus seemed to be that "auto pure" is more confusing than its worth.
 2022-02-03 16:25:24 -08:00
Leonardo de Moura
5f74cd4968 feat: add let pat := val | elseCase do-notation 2022-02-03 15:55:03 -08:00
Leonardo de Moura
420f5bb315 fix: hide internal namespaces from autocompletion 
closes #993
 2022-02-03 13:33:27 -08:00
Leonardo de Moura
17eab845ed fix: improve tryPostponeIfMVar 
see #992
 2022-02-03 13:24:19 -08:00
Leonardo de Moura
42b3ed5903 test: add Pi.single test 
see #988
 2022-02-03 09:22:22 -08:00
Gabriel Ebner
54cff10f3f fix: dependent fields in diamond extensions 2022-02-03 09:17:14 -08:00
Leonardo de Moura
c30380e2fa feat: lift the restriction in congr theorems that all function arguments on the lhs must be free variables 
see #988
 2022-02-02 18:23:18 -08:00
Leonardo de Moura
b7c853692d test: add test for decide congruence issue 
TODO: congruence lemma must be automatically generated.

see #988
 2022-02-02 17:49:03 -08:00
Leonardo de Moura
101fc12b54 feat: partially applied user congruence lemmas 
see #988
 2022-02-02 17:41:21 -08:00