Leonardo de Moura
|
772beeeb29
|
feat: add withAtLeastMaxRecDepth
|
2022-09-19 22:04:04 -07:00 |
|
Leonardo de Moura
|
4c19fdbb97
|
fix: normFVarImp bug
|
2022-09-19 21:41:18 -07:00 |
|
Leonardo de Moura
|
d132efd440
|
feat: polymorphic Code.bind
|
2022-09-19 21:41:18 -07:00 |
|
Mario Carneiro
|
356db4e1df
|
fix: simplify termination_by clause
|
2022-09-19 13:49:20 -07:00 |
|
Mario Carneiro
|
2f8d20a90d
|
fix: fix test
|
2022-09-19 13:49:20 -07:00 |
|
Mario Carneiro
|
bb23fc0c86
|
chore: extract termination lemma for reverse
|
2022-09-19 13:49:20 -07:00 |
|
Mario Carneiro
|
ed6a5bba88
|
chore: rename insertAt to insertAt!
|
2022-09-19 13:49:20 -07:00 |
|
Mario Carneiro
|
f8c6306469
|
feat: remove bounds checks in Array.{reverse, insertAt}
|
2022-09-19 13:49:20 -07:00 |
|
Leonardo de Moura
|
ad0f8d3258
|
chore: update stage0
|
2022-09-19 12:47:44 -07:00 |
|
Gabriel Ebner
|
27525f33fb
|
fix: changes due to requiring colEq
|
2022-09-19 12:44:43 -07:00 |
|
Gabriel Ebner
|
a351a4be70
|
feat: use colEq in sepByIndent
|
2022-09-19 12:44:43 -07:00 |
|
Gabriel Ebner
|
b1bef71d59
|
feat: colEq parser
|
2022-09-19 12:44:43 -07:00 |
|
Mario Carneiro
|
61df1e5073
|
feat: expose that panic α = default
|
2022-09-19 08:59:08 -07:00 |
|
Yuri de Wit
|
88fc24c58c
|
chore: fixed typos
|
2022-09-19 08:14:37 -07:00 |
|
Sebastian Ullrich
|
3ef1baae4a
|
doc: refine mdbook docs
|
2022-09-19 06:30:11 -07:00 |
|
Leonardo de Moura
|
800938065a
|
chore: update stage0
|
2022-09-18 17:10:58 -07:00 |
|
Gabriel Ebner
|
9113291e9e
|
fix: preserve separators in evalSepByIndentConv
|
2022-09-18 16:43:23 -07:00 |
|
Gabriel Ebner
|
3add955382
|
fix: preserve separators in evalSepByIndentTactic
|
2022-09-18 16:43:23 -07:00 |
|
Gabriel Ebner
|
ee9c9b1312
|
feat: skip final newline in sepByIndent format
|
2022-09-18 16:43:23 -07:00 |
|
Gabriel Ebner
|
0e01d855b0
|
chore: fix test
|
2022-09-18 16:43:23 -07:00 |
|
Gabriel Ebner
|
ca4dfa5627
|
chore: update stage0
|
2022-09-18 16:43:23 -07:00 |
|
Gabriel Ebner
|
193a18e4e3
|
Revert "hack: support group tactic for bootstrap"
|
2022-09-18 16:43:23 -07:00 |
|
Gabriel Ebner
|
2b5c1e397a
|
feat: use sepBy1Indent for conv blocks
|
2022-09-18 16:43:23 -07:00 |
|
Gabriel Ebner
|
7cc70fe375
|
chore: update stage0
|
2022-09-18 16:43:23 -07:00 |
|
Gabriel Ebner
|
74a75e75c8
|
hack: support group tactic for bootstrap
|
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 |
|
Gabriel Ebner
|
9b8b7264f8
|
chore: prepare for bootstrap
|
2022-09-18 16:43:23 -07:00 |
|
Leonardo de Moura
|
b50a3c72e9
|
fix: missing headBetas
|
2022-09-18 15:52:19 -07:00 |
|
Leonardo de Moura
|
4df303900b
|
feat: apply specialize to specialized code recursively
|
2022-09-18 15:42:44 -07:00 |
|
Leonardo de Moura
|
70f615d074
|
fix: avoid "unknown constant" error message for auxiliary declarations
|
2022-09-18 15:39:58 -07:00 |
|
Leonardo de Moura
|
5fbe63cca4
|
fix: process remaining params
|
2022-09-18 15:29:41 -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
|
796e9e3bdd
|
feat: eta expand at specializeApp?
|
2022-09-18 13:21:55 -07:00 |
|
Leonardo de Moura
|
9dede6f632
|
feat: add mkSpecDecl
|
2022-09-17 17:30:57 -07:00 |
|
Leonardo de Moura
|
483234f30c
|
refactor: rename Internalize.M
|
2022-09-17 16:46:44 -07:00 |
|
Leonardo de Moura
|
27c504107e
|
feat: universe level parameter helper functions for the compiler
|
2022-09-17 16:29:44 -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 |
|
E.W.Ayers
|
4b562438f8
|
doc: MetavarContext
|
2022-09-16 09:13:47 -07:00 |
|
E.W.Ayers
|
993115a937
|
feat: Kleisli operators
|
2022-09-16 05:49:56 -07:00 |
|
Elias Aebi
|
085f51ecb9
|
doc: fix Markdown code-blocks
|
2022-09-16 05:48:44 -07:00 |
|
Leonardo de Moura
|
abe1f7f6f9
|
feat: dependency collector for the code specializer
|
2022-09-15 19:55:37 -07:00 |
|
Leonardo de Moura
|
ef636f6ec5
|
chore: update stage0
|
2022-09-15 19:02:37 -07:00 |
|
Leonardo de Moura
|
b77ff79133
|
fix: put Lean.Server.FileWorker.WidgetRequests back
|
2022-09-15 19:02:12 -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 |
|
Mario Carneiro
|
eac410db4e
|
fix: fix tests
|
2022-09-15 14:02:38 -07:00 |
|
Mario Carneiro
|
c0812d0673
|
chore: reorder Elab.MutualDef and Elab.Deriving.Basic
|
2022-09-15 14:02:38 -07:00 |
|