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
Mario Carneiro
0961561d4e
feat: track simp lemmas through the core tactics
2022-09-25 06:40:56 -07:00
Leonardo de Moura
f9abcae4e4
chore: simplify tactic macro
...
The `[inlineIfReduce]` at `List.toArrayAux` is currently very
expensive, and this example produces a deep recursion when inlining
the `List.toArrayAux` applications.
2022-09-24 19:53:04 -07:00
Leonardo de Moura
ce12ecfe13
fix: free variable collision at LCNF/Specialize.lean
2022-09-24 18:51:32 -07:00
Leonardo de Moura
871644fe8b
chore: fix tests
2022-09-24 15:20:44 -07:00
Leonardo de Moura
ce90e98648
feat: activate new compiler first phase
2022-09-24 14:20:21 -07:00
Leonardo de Moura
b88bd98afa
fix: unreach case for Code.bind
2022-09-24 08:13:17 -07:00
Leonardo de Moura
947811cab8
fix: zero exit points != one exit point
2022-09-24 08:13:17 -07:00
Leonardo de Moura
85c468c853
fix: remove internal name hack at [specialize] and [inline] attributes
2022-09-23 20:25:16 -07:00
Leonardo de Moura
011521013d
feat: use phase at inferConstType, save specialization
2022-09-23 16:45:04 -07:00
Leonardo de Moura
1e846ae280
test: for LCNF
2022-09-23 14:02:34 -07:00
Leonardo de Moura
4323205185
fix: support user-defined empty inductives at toLCNF
2022-09-23 05:50:02 -07:00
Leonardo de Moura
0b4590bd69
test: add erased.lean
2022-09-23 05:29:42 -07:00
Leonardo de Moura
eed569153b
fix: dependent field issue
2022-09-22 20:38:42 -07:00
Leonardo de Moura
412a05d0d6
fix: ensure cases field parameters do not occur in types
2022-09-22 20:15:39 -07:00
Leonardo de Moura
c0ac2138f7
fix: ensure inferForallType at LCNF handles universes like the kernel and MetaM
2022-09-22 16:38:16 -07:00
Leonardo de Moura
1437b9cd90
fix: non-termination when eta-expanding Eq.ndrec at toLCNF
2022-09-22 16:04:19 -07:00
Leonardo de Moura
f721e44718
fix: simplify compatibleTypes
...
Add note about "erasure confusion" in LCNF.
2022-09-22 15:15:32 -07:00
Leonardo de Moura
708a777d74
test: add more LCNF tests
2022-09-21 21:12:17 -07:00
Mario Carneiro
9faca046d6
fix: fix test
2022-09-21 18:04:31 -07:00
Leonardo de Moura
727ee79f05
fix: exponential blowup at LCNF simp
2022-09-20 17:03:40 -07:00
Mario Carneiro
a74892a36b
feat: multiple case
2022-09-20 14:15:37 -07:00
Gabriel Ebner
7356840cbc
feat: use sepBy1Indent for tactic blocks
2022-09-18 16:43:23 -07:00
