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
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
