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

3623 commits

Author SHA1 Message Date
Leonardo de Moura
1c1e6d79a7 feat: add equality proof for named patterns 
The user can optionally name the equality proof.
The new test demostrates how to name the equality proof.

closes #501
 2022-01-18 12:43:01 -08:00
Leonardo de Moura
cd903bde77 refactor: [s : Setoid α] => {s : Setoid α} or (s : Setoid α) 
See comment at https://github.com/leanprover/lean4/issues/952#issuecomment-1015265136

cc @gebner
 2022-01-18 09:24:06 -08:00
Leonardo de Moura
da06bb6605 fix: matching inside new termination_by 2022-01-17 08:47:05 -08:00
Leonardo de Moura
189f4bd372 chore: fix tests 2022-01-15 12:18:09 -08:00
Leonardo de Moura
b0d9c16c7a chore: rename PointedType => NonemptyType 2022-01-15 11:43:53 -08:00
Leonardo de Moura
e3241e82bc feat: define PointedType as { α : Type u // Nonempty α } 2022-01-14 20:36:51 -08:00
Leonardo de Moura
1620987b6c fix: recursive applications in discriminants 2022-01-13 09:56:33 -08:00
Leonardo de Moura
3fbf5acbee fix: add missing [reducible] annotations Init/WF.lean 2022-01-12 17:12:55 -08:00
Leonardo de Moura
98864f707e test: add test for #879 
The new `termination_by` syntax should address issue #879

closes #879
 2022-01-12 16:25:09 -08:00
Leonardo de Moura
9162901c86 fix: expandTerminationByNonCore 2022-01-12 16:22:54 -08:00
Leonardo de Moura
91a0ac8a12 feat: elaborate new termination_by syntax 2022-01-12 16:15:30 -08:00
Leonardo de Moura
111d09fda3 fix: must apply afterCompilation attributes *after* smart unfolding definition was declared 
The `[simp]` attribute checks whether the smart unfolding defintion
has been declared.

closes #946
 2022-01-12 08:28:03 -08:00
Leonardo de Moura
45bd328d5e fix: tests and add WellFoundedRelation.rel to list of definitions to unfold at decreasing_tactic 2022-01-12 08:28:03 -08:00
Leonardo de Moura
068cc700d8 test: ackermann 2022-01-11 15:03:07 -08:00
Leonardo de Moura
381f66428a chore: use termination_by' 
We are going to define a higher level syntax for `termination_by`.
 2022-01-11 15:00:53 -08:00
Leonardo de Moura
4c918a2363 feat: use default_decreasing_tactic at WF/Fix.lean 2022-01-10 14:55:38 -08:00
Leonardo de Moura
0dd3ce0598 chore: fix test 2022-01-10 14:31:23 -08:00
Leonardo de Moura
b797c982fc feat: add mkUnfoldProof 2022-01-07 13:51:45 -08:00
Mario Carneiro
dcaf3c615f fix: induction generalizing precedence 2022-01-07 10:45:45 +01:00
Leonardo de Moura
bef161caf7 feat: add better support for discharging equation theorem hypotheses 2022-01-06 14:42:23 -08:00
Leonardo de Moura
90b179bea9 fix: add equation theorems even if definition supports smart unfolding 
See new test.
 2022-01-06 13:53:03 -08:00
Leonardo de Moura
d8d7d63830 fix: registers eqns info before adding definition 
Otherwise `[simp]` at definition will fail to generate equational theorems.
 2022-01-06 12:24:40 -08:00
Leonardo de Moura
7acbbb4fbb fix: auxiliary whnfAux used at mkEqns 2022-01-06 09:57:41 -08:00
Leonardo de Moura
60934bf1d5 feat: add support for removing [simp] attribute from definitions with equational theorems 2022-01-05 16:57:59 -08:00
Leonardo de Moura
c2e52bd577 feat: use getEqnsFor? when applying [simp] at definitions 2022-01-05 15:59:39 -08:00
Leonardo de Moura
030e932db8 feat: use getEqnsFor? at simp 2022-01-05 11:28:24 -08:00
Leonardo de Moura
4d1343d670 chore: use _eq instead of eq to name auto generated equational theorems 2022-01-04 17:23:34 -08:00
Leonardo de Moura
b2918e0c76 test: add tests for WF.mkEqns 2022-01-04 17:18:51 -08:00
Leonardo de Moura
d782a97f5c feat: add WF.mkProof for WF.mkEqns 2022-01-04 17:00:54 -08:00
Leonardo de Moura
b9f7d1defb fix: constant folding after erasure 
closes #909
 2022-01-03 10:33:07 -08:00
Gabriel Ebner
e605c541d0 fix: do not infer type in erase_irrelevant 
At the time erase_irrelevant is called, we have already eliminated the
`cast`-applications.  Therefore non-atomic expressions may no longer
be well-typed (and `infer_type` can fail).
 2022-01-03 07:13:55 -08:00
Sebastian Ullrich
555584375a fix: compare fields top-down in deriving Ord 2022-01-03 07:02:13 -08:00
Leonardo de Moura
be6bc67eb0 fix: ensure match-expressions compiled using if-then-else can be reduced with TransparencyMode.reducible 
closes #891
 2021-12-18 10:55:42 -08:00
Leonardo de Moura
c954fc9ec7 fix: bug at simpLoop 2021-12-18 06:48:08 -08:00
Leonardo de Moura
0a81093db5 fix: bug at simpProj 
This bug was reported at https://github.com/dwrensha/lean4-maze/issues/1
 2021-12-15 17:07:00 -08:00
Gabriel Ebner
7e483d3a0a feat: support syntax abbreviations in dynamic quotations 2021-12-15 11:17:58 +00:00
Leonardo de Moura
b6ef65d8fd fix: where structure instance parser 
closes #753
 2021-12-12 07:52:52 -08:00
Leonardo de Moura
a3361e7d86 fix: missing universe assignments made during TC resolution 
closes #796
 2021-12-12 07:07:13 -08:00
Leonardo de Moura
483f32edd8 feat: in pure code, do use assume Id monad at do notation 
This feature produced counterintuitive behavior and confused users.
See discussion at #770.

As pointed out by @tydeu, it is not too much work to write `Id.run <|`
before the `do` when we want to use the `do` notation in pure code.

closes #770
 2021-12-10 12:55:14 -08:00
Leonardo de Moura
96e0e1db98 fix: nontermination at simp [OfNat.ofNat] 
closes #788
 2021-12-10 12:29:33 -08:00
Leonardo de Moura
e64cfbb9b2 test: well-founded recursion example 
see #860
 2021-12-09 14:32:06 -08:00
Leonardo de Moura
41040a81de fix: auxiliary matcher definitions should be treated as abbreviations 
The motivation is to prevent performance problems such as the one
described at issue #854.

Fixes #854 after a update stage0
 2021-12-07 16:43:20 -08:00
Leonardo de Moura
b0fe1e5d10 feat: add Tomas Skrivan's TC resolution improvement 
This commit implements the TC resolution improvement suggested by
Tomas at #815.

Closes #815.
 2021-12-06 17:46:11 -08:00
Sebastian Ullrich
80c3d88e3e refactor: optimize critical import path 2021-12-06 08:05:24 -08:00
Leonardo de Moura
b2d88f7bcc fix: bug at saveEqn 2021-12-02 17:38:39 -08:00
Leonardo de Moura
bb768b06cd feat: add PersistentArray.foldrM 2021-12-02 17:17:55 -08:00
Leonardo de Moura
c42196440f fix: give preference to non-indices at findRecArg 
fixes #837
 2021-12-01 16:45:19 -08:00
Sebastian Ullrich
465913c391 fix: this must be a keyword 2021-11-29 10:06:15 -08:00
Sebastian Ullrich
531eefb7db chore: adapt syntax 2021-11-29 10:06:15 -08:00
Leonardo de Moura
0aa32d643e fix: eta struct and proof irrelevance issue 
see #777
 2021-11-27 07:15:57 -08:00