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

4148 commits

Author SHA1 Message Date
Sebastian Ullrich
591eccee4f chore: move expensive test to beginning of test block 2022-11-14 15:46:34 +01:00
Leonardo de Moura
5654d8465d fix: fixes #1822 2022-11-13 18:13:29 -08:00
Leonardo de Moura
a87f0e25de feat: add compiler.checkTypes for sanity checking 2022-11-13 17:45:21 -08:00
Leonardo de Moura
ca0fb21df4 fix: fixes #1813 
Remark: modifies the value for the `mid` priority.
See new note at `Init/Notation.lean`
 2022-11-10 16:09:21 -08:00
Leonardo de Moura
c147059fd7 fix: fixes #1812 2022-11-10 08:58:09 -08:00
Leonardo de Moura
b4d13a8946 refactor: LetExpr => LetValue 
We use "let value" in many other places in the code base.
 2022-11-07 18:51:07 -08:00
Leonardo de Moura
d11697cbf7 chore: fix some tests 2022-11-07 18:18:06 -08:00
Scott Morrison
d0dc9a2f90
fix: reorder goals after specialize (#1796) 
* fix: reorder goals after specialize

* fix test
 2022-11-03 06:32:55 -07:00
Mario Carneiro
ad1c23f172 fix: bug in replaceLocalDeclDefEq 
fixes #1615
 2022-11-01 19:18:25 -07:00
Leonardo de Moura
5f38a483f2 fix: congr tactic 
`MVarId.congr?` and `MVarId.hcongr?` should return `none` if an
exception is thrown while applying congruence theorem.

`MVarId.hcongr?` should try `eq_of_heq` before trying to apply
`hcongr` theorem.

closes #1787

BTW: Lean 4 `congr` tactic is applying `assumption`. Lean 3 version does not.
 2022-10-28 08:00:04 -07:00
Leonardo de Moura
0b6b754bca feat: improve apply tactic 
It tries to address what the Mathlib community calls the "apply bug".

cc @digama0
 2022-10-26 16:58:43 -07:00
Leonardo de Moura
f3b1eadb55 feat: copy docstring when copying parent fields 
closes #1730
 2022-10-26 15:43:46 -07:00
Leonardo de Moura
83d8e36773 fix: fixes #1780 2022-10-26 07:46:38 -07:00
Leonardo de Moura
5a8f9ace72 fix: open .. hinding .. should activate scoped attributes 2022-10-26 07:39:06 -07:00
Gabriel Ebner
725aa8b39a refactor: instantiateTypeLevelParams in Lean 2022-10-24 12:23:13 -07:00
Gabriel Ebner
fc304d95c0 feat: Min/Max typeclasses 2022-10-21 14:36:38 -07:00
Leonardo de Moura
aeddcbdc6d fix: disable implicit lambdas at intro <pattern> notation 
See issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/intro.20with.20type.20specified/near/305150215
 2022-10-20 09:04:06 -07:00
Mario Carneiro
dd8bbe9367 fix: catch kernel exceptions in Kernel.{isDefEq, whnf} 
fixes #1756
 2022-10-20 05:38:29 -07:00
Mario Carneiro
dd5948d641 chore: snake-case attributes (part 1) 2022-10-19 09:28:08 -07:00
Gabriel Ebner
0c2a5580cb feat: enforce correct syntax kind in macros 2022-10-18 14:59:14 -07:00
Gabriel Ebner
fb4d90a58b feat: dynamic quotations for categories 2022-10-18 14:59:14 -07:00
Leonardo de Moura
9244a7a8a5 fix: ensure old and new compiler auxiliary declaration names do not collide 2022-10-16 14:49:55 -07:00
Leonardo de Moura
6378283fa8 feat: add Probe.toString 2022-10-14 19:21:56 -07:00
Henrik Böving
38788a72be feat: basic compiler probing framework with examples 2022-10-14 19:09:35 -07:00
Gabriel Ebner
1c561c39a8 feat: function coercions with unification 2022-10-14 12:08:10 -07:00
Leonardo de Moura
7308fa0e7d feat: ensure lambda lifter is creating unused names 2022-10-12 16:35:55 -07:00
Gabriel Ebner
79569c9003 chore: replace let by have in stx matches 2022-10-12 11:52:28 -07:00
Gabriel Ebner
6593bd98b3 chore: add test for 1692 2022-10-11 17:24:35 -07:00
Gabriel Ebner
ba57ad3480 feat: add implementation-detail hypotheses 2022-10-11 17:24:35 -07:00
Leonardo de Moura
525b4f761c chore: fix tests 2022-10-10 17:48:32 -07:00
Henrik Böving
dd3c0f77f1 feat: FloatLetIn compiler pass 2022-10-10 23:56:20 +02:00
Leonardo de Moura
7b3709e28a chore: simplify proof in test for #1711 
TODO: improve support for instance implicit arguments at `congr`
 2022-10-10 07:29:53 -07:00
Leonardo de Moura
0041de5d1d fix: congr tactic should not try to synthesize instance implicit arguments that have been inferred when applying congr theorem 
see #1711
 2022-10-10 07:24:27 -07:00
Leonardo de Moura
cc09afc5e1 fix: type error introducing when inlining LCNF functions 
This issue has been reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Annoying.20LCNF.20errors/near/303142516
 2022-10-09 12:10:11 -07:00
Mario Carneiro
d4219c9d70 fix: List.Mem should have two parameters 2022-10-09 05:46:52 -07:00
Leonardo de Moura
6bc4144409 fix: fixes #1549 2022-10-08 07:41:49 -07:00
Leonardo de Moura
e3ec468e3b fix: fixes #1650 2022-10-07 19:00:23 -07:00
Leonardo de Moura
45974229d2 feat: reactivate extendJoinPointContext at mono phase 
closes #1686

cc @hargoniX
 2022-10-07 16:27:44 -07:00
Leonardo de Moura
1b8e310ada fix: fixes #1674 2022-10-07 13:33:41 -07:00
Leonardo de Moura
adeab12beb feat: add support for Iff.rec and Iff.casesOn to new code generator 
closes #1684
 2022-10-04 06:32:49 -07:00
Leonardo de Moura
c4db085ac1 fix: missing dependency check at simpJpCases? 2022-10-03 19:39:10 -07:00
Leonardo de Moura
fed7ff27e8 fix: issue reported on Zulip 
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Annoying.20LCNF.20errors/near/302056742
 2022-10-03 09:51:32 -07:00
Leonardo de Moura
31d59e337b fix: LCNF any type issue 
This fixes an issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Annoying.20LCNF.20errors/near/301935406
 2022-10-02 08:09:13 -07:00
Leonardo de Moura
e5494e7a49 fix: eta-expansion at compatibleTypes 
It fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Annoying.20LCNF.20errors/near/301424293
 2022-09-29 11:02:06 -07:00
Leonardo de Moura
94c2ec38d5 feat: implement cast TODO 
fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Annoying.20LCNF.20errors/near/301269857
 2022-09-28 15:40:53 -07:00
Leonardo de Moura
135790f41a fix: missing eraseCode at inlineProjInst? 
Fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/LCNF.20local.20context.20contains.20unused.20local.20variable.20declaratio/near/301102923
 2022-09-27 16:26:49 -07:00
Mario Carneiro
85119ba9d1 chore: move Std.* data structures to Lean.* 2022-09-26 05:46:04 -07:00
Mario Carneiro
121b18f40a chore: add test 2022-09-25 06:42:20 -07:00
Mario Carneiro
47930c6fd1 fix: fix tests 2022-09-25 06:40:56 -07:00
Mario Carneiro
9a9f3263d4 feat: add tactic.simp.trace option 2022-09-25 06:40:56 -07:00