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
Ed Ayers
2a6697e077
feat: goal-diffs ( #1610 )
2022-09-24 11:46:11 +02: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
8c84531330
chore: fix test
2022-09-22 16:10:12 -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
Leonardo de Moura
a2bcb3b73e
fix: erase propositon formers, add isErasedCompatible, remove approx. from compatibleTypes
2022-09-21 20:47:02 -07:00
Leonardo de Moura
f362de995b
chore: fix tests
2022-09-21 18:17:32 -07:00
Mario Carneiro
9faca046d6
fix: fix test
2022-09-21 18:04:31 -07:00
Mario Carneiro
ef0736c303
feat: multiple delta (part 2)
2022-09-21 18:04:31 -07:00
Mario Carneiro
b922483ebc
chore: remove getElem' delab
2022-09-21 06:21:00 -07:00
Mario Carneiro
20937c3a6c
fix: fix test
2022-09-21 06:21:00 -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
Mario Carneiro
2f8d20a90d
fix: fix test
2022-09-19 13:49:20 -07:00
Gabriel Ebner
a351a4be70
feat: use colEq in sepByIndent
2022-09-19 12:44:43 -07:00
Gabriel Ebner
3add955382
fix: preserve separators in evalSepByIndentTactic
2022-09-18 16:43:23 -07:00
Gabriel Ebner
0e01d855b0
chore: fix test
2022-09-18 16:43:23 -07:00
Gabriel Ebner
7356840cbc
feat: use sepBy1Indent for tactic blocks
2022-09-18 16:43:23 -07:00
Leonardo de Moura
90b9b0b7e9
chore: move compiler tests to run folder
2022-09-18 15:08:52 -07:00
Leonardo de Moura
05145577fd
feat: cache specialization results
2022-09-18 14:53:18 -07:00
Leonardo de Moura
db6ee72aed
chore: typo
2022-09-17 09:55:46 -07:00
Leonardo de Moura
50fe9ceeaa
test: more tests for new compiler
2022-09-16 18:00:27 -07:00
Leonardo de Moura
3c6dee8048
fix: LCNF eta expansion bug at Simp.lean
2022-09-16 18:00:27 -07:00
Leonardo de Moura
c16d4fb926
chore: fix test suite
2022-09-15 18:59:51 -07:00
Leonardo de Moura
d3b0b49c43
feat: improve elabBinRelCore
...
See new test and comments at `elaBinRelCore`
2022-09-15 15:17:57 -07:00
