Leonardo de Moura
c4db085ac1
fix: missing dependency check at simpJpCases?
2022-10-03 19:39:10 -07:00
Leonardo de Moura
da4812659c
feat: use DiscrM to implement simpJpCases?
2022-10-03 19:13:31 -07:00
Leonardo de Moura
f0be5439e6
feat: JpCases for join points with multiple parameters
2022-10-03 18:35:16 -07:00
Henrik Böving
eaab29712d
feat: extend join point context pass
2022-10-03 17:03:22 -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
7857995df4
fix: fixes #1673
2022-10-02 08:23:14 -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
190a1331bd
feat: add toMonoType
2022-10-01 20:44:31 -07:00
Leonardo de Moura
1ce9e30403
refactor: extension for storing LCNF types for declarations that do not have code associated with them
2022-10-01 20:44:31 -07:00
pcpthm
96b49261e6
fix: derive Repr missing a comma
2022-10-01 07:17:57 -07:00
Leonardo de Moura
15909f209f
feat: inline small declarations not tagged with [noinline]
2022-09-30 20:51:37 -07:00
Leonardo de Moura
0e18b4318c
feat: online inline recursive functions if they are tagged with [inlineIfReduce]
2022-09-30 19:39:12 -07:00
Mario Carneiro
9aa57f9959
fix: .ident hover in patterns
2022-09-30 15:18:06 -07:00
Leonardo de Moura
fb1a603e60
feat: add another CSE pass before saveBase
2022-09-29 18:56:20 -07:00
Leonardo de Moura
5746338c15
fix: mark Lean.Name.mkStr* functions as [reducible]
...
This is needed for type checking `TSyntax`.
2022-09-29 17:36:30 -07:00
Leonardo de Moura
126da8185d
feat: more compact quotations
...
Trying to control the generated code size.
2022-09-29 16:56:43 -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
Mario Carneiro
66040a9803
feat: clearer info tree formatting
2022-09-29 19:07:18 +02:00
Mario Carneiro
7a6f7cb0ac
fix: induction info tree nesting
2022-09-29 19:07:18 +02:00
Mario Carneiro
73f44ccb7b
feat: hover for cases/induction case names
2022-09-29 19:07:18 +02:00
Leonardo de Moura
73ebaf8499
feat: improve visitLambda at toLCNF
2022-09-28 19:17:28 -07:00
Sebastian Ullrich
d0a002ffff
fix: prefer longer parse even if unsuccessful
2022-09-28 15:57:01 -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
Mario Carneiro
1c992fde37
chore: add some tests
2022-09-28 14:24:44 -07:00
Mario Carneiro
b6a58d13e1
fix: LHS goals should be pre-whnf'd
2022-09-28 14:24:44 -07:00
Ed Ayers
10971a413a
feat: fromJson? derivations now say where a parsing error occurred ( #1656 )
2022-09-28 09:15:26 +00:00
Leonardo de Moura
fd5f3a5bad
feat: track recursively inlining
...
closes #1657
see #1646
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/inline.20codegen.20crash/near/301099703
2022-09-27 16:26:49 -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
d843e2a418
chore: add docs and test
2022-09-27 22:09:54 +02:00
Mario Carneiro
280d8c9c9b
feat: add (canonical := true) option in Syntax
2022-09-27 22:09:54 +02:00
Mario Carneiro
85119ba9d1
chore: move Std.* data structures to Lean.*
2022-09-26 05:46:04 -07:00
Leonardo de Moura
fd1ae3118c
feat: replace isCasesOnCases? with simpJpCases?
...
It addresses the code explosion issue with the old optimization.
For example, the resulting size for `Lean.Json.Parser.escapedChar`
went from 31593 to 361.
2022-09-25 20:57:24 -07:00
Mario Carneiro
9b9998f5c8
feat: pattern (occs := ...) conv
2022-09-25 19:52:56 -07:00
Mario Carneiro
5644bd7a3f
feat: show decl module in hover
2022-09-25 06:43:48 -07:00
Mario Carneiro
121b18f40a
chore: add test
2022-09-25 06:42:20 -07:00
Mario Carneiro
b287658dc3
chore: add test with <->, discharger, contextual, conditional
2022-09-25 06:40:56 -07:00
Mario Carneiro
47930c6fd1
fix: fix tests
2022-09-25 06:40:56 -07:00
Mario Carneiro
606328aceb
feat: improve simp theorem tracing
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
Sebastian Ullrich
381a643fd0
chore: make rbmap.hs more similar to other implementations
2022-09-24 14:16:48 +02:00
Sebastian Ullrich
77e42744dd
chore: modernize rbmap benchmarks a bit
2022-09-24 14:16:48 +02:00
Sebastian Ullrich
9f29967fb0
chore: add rbmap.library benchmark to bench suite
2022-09-24 12:35:08 +02:00
Ed Ayers
2a6697e077
feat: goal-diffs ( #1610 )
2022-09-24 11:46:11 +02:00
