Henrik Böving
|
fe63bd2e8e
|
feat: basic pass manager
|
2022-08-31 16:28:07 -07:00 |
|
Sebastian Ullrich
|
98145ad8ba
|
chore: not a docstring
|
2022-08-31 22:19:27 +02:00 |
|
Mario Carneiro
|
ebb5b97d73
|
chore: move Bootstrap.Data -> Lean.Data
|
2022-08-31 11:48:57 -07:00 |
|
Mario Carneiro
|
c089639b19
|
refactor: Init.SimpLemmas proof golf / cleanup
|
2022-08-31 11:27:58 -07:00 |
|
Leonardo de Moura
|
2fc38fb118
|
feat: instantiateTypeLevelParams and instantiateValueLevelParams for LCNF.Decl
|
2022-08-30 20:20:39 -07:00 |
|
Leonardo de Moura
|
a0b47195ba
|
fix: fixes #1547
|
2022-08-30 11:45:05 -07:00 |
|
Leonardo de Moura
|
b6f0bdc542
|
chore: add Array.mapMono
|
2022-08-30 11:45:05 -07:00 |
|
Leonardo de Moura
|
c451bf0c91
|
feat: add simpFunDecl
|
2022-08-30 11:45:05 -07:00 |
|
Mario Carneiro
|
b2b02295b0
|
chore: move ShareCommon to Init / Lean
|
2022-08-30 07:51:43 -07:00 |
|
Leonardo de Moura
|
ca80bc52dc
|
feat: LCNF.simp .let case
|
2022-08-29 09:52:16 -07:00 |
|
Leonardo de Moura
|
7b161d33d1
|
refactor: add MonadFVarSubst class
|
2022-08-29 09:52:16 -07:00 |
|
Mario Carneiro
|
6a7ccb5797
|
refactor: generalize ShareCommon to a typeclass (#1537)
|
2022-08-29 09:34:38 -07:00 |
|
Mario Carneiro
|
850ee17346
|
chore: move Bootstrap.System.Uri to Init
|
2022-08-29 08:06:30 -07:00 |
|
Siddharth Bhat
|
a7b128fee1
|
doc: explanations for LCNF.
|
2022-08-29 07:17:25 -07:00 |
|
Mario Carneiro
|
0efbc0bc03
|
chore: remove BinomialHeap, DList, Stack, Queue
These are moving to std4.
|
2022-08-29 07:07:53 -07:00 |
|
Mario Carneiro
|
bf89c5a0f5
|
chore: move Std -> Bootstrap
|
2022-08-29 01:26:12 -07:00 |
|
Mario Carneiro
|
31784c9a24
|
doc: documentation for Init.Core
|
2022-08-29 00:41:24 -07:00 |
|
Mario Carneiro
|
5658000396
|
refactor: golf proof of funext
|
2022-08-28 19:01:46 -07:00 |
|
Leonardo de Moura
|
062d4728a1
|
feat: more LCNF update functions
and bug fixes at CSE
|
2022-08-28 19:00:49 -07:00 |
|
Leonardo de Moura
|
5552d610e8
|
chore: missing updateCases!
|
2022-08-28 16:30:54 -07:00 |
|
Leonardo de Moura
|
e80028b7d1
|
feat: add pure field to LetDecl, add helper functions for updating LCNF code
The update functions try to minimize the amount of memory allocation
|
2022-08-28 08:55:35 -07:00 |
|
Leonardo de Moura
|
4f5a014170
|
feat: add Array.mapMonoM
|
2022-08-28 08:55:35 -07:00 |
|
Leonardo de Moura
|
d5fa178fc3
|
feat: modify FVarSubst used in the new code generator
|
2022-08-28 08:55:35 -07:00 |
|
Leonardo de Moura
|
6a9f8ad919
|
fix: Compiler/LCNF/ElimDead.lean
|
2022-08-28 08:55:35 -07:00 |
|
Mario Carneiro
|
f93914e613
|
fix: prove decidable_of_decidable_of_eq without cast
|
2022-08-28 08:32:00 -07:00 |
|
Mario Carneiro
|
d4c7d0f266
|
chore: remove def implies
|
2022-08-28 07:57:56 -07:00 |
|
Leonardo de Moura
|
cd0dd4cc2f
|
feat: start simp for new LCNF format
|
2022-08-27 19:59:31 -07:00 |
|
Leonardo de Moura
|
9446ae3056
|
feat: add cleanup function for CompilerM
|
2022-08-27 18:35:30 -07:00 |
|
Leonardo de Moura
|
30d8ae70f7
|
chore: remove workarounds
|
2022-08-27 10:56:15 -07:00 |
|
Leonardo de Moura
|
ee8e771445
|
fix: dotted name bug
|
2022-08-27 10:41:55 -07:00 |
|
Leonardo de Moura
|
0f40dfc063
|
feat: add FunDecl.etaExpand
|
2022-08-27 10:41:54 -07:00 |
|
Leonardo de Moura
|
11c8253f6c
|
feat: more update functions for LCNF
|
2022-08-27 10:41:54 -07:00 |
|
Leonardo de Moura
|
bdf89b4d85
|
chore: add {crossEmoji} at failure
|
2022-08-27 10:41:54 -07:00 |
|
Sebastian Ullrich
|
fb408c024b
|
fix: deleting built-in docstrings
|
2022-08-27 17:19:25 +02:00 |
|
Mario Carneiro
|
9bd886f37d
|
fix: @[inheritDoc] on notation
|
2022-08-27 07:11:39 -07:00 |
|
Leonardo de Moura
|
0925051c51
|
chore: rename Reader to ReaderM
closes #1524
|
2022-08-26 20:59:17 -07:00 |
|
Sebastian Ullrich
|
12d7e839b0
|
doc: Stream.read/getLine
|
2022-08-26 20:55:09 -07:00 |
|
Sebastian Ullrich
|
b010805000
|
fix: Handle.read at EOF
|
2022-08-26 20:55:09 -07:00 |
|
Sebastian Ullrich
|
a69d7fb018
|
fix: remove broken Handle.isEof
|
2022-08-26 20:55:09 -07:00 |
|
Sebastian Ullrich
|
d23c19884b
|
doc: read/getLine EOF behavior
|
2022-08-26 20:55:09 -07:00 |
|
Sebastian Ullrich
|
af7f5aa2a0
|
feat: dbgStackTrace
|
2022-08-26 20:52:51 -07:00 |
|
E.W.Ayers
|
f52a1bd37c
|
doc: JSON-RPC
|
2022-08-26 20:49:57 -07:00 |
|
E.W.Ayers
|
4ea4365354
|
doc: various String docstrings
|
2022-08-26 20:49:57 -07:00 |
|
E.W.Ayers
|
3aeb3db3b5
|
doc: Char/Basic.lean
|
2022-08-26 20:49:57 -07:00 |
|
E.W.Ayers
|
5611620d3a
|
dov: explanation of why pointers aren't sound.
|
2022-08-26 20:49:57 -07:00 |
|
E.W.Ayers
|
152d441a4c
|
doc: note that Float.beq is not refl
|
2022-08-26 20:49:57 -07:00 |
|
Leonardo de Moura
|
969dce70db
|
perf: improve FVarSubst apply functions in the new compiler stack
|
2022-08-26 20:10:36 -07:00 |
|
Mario Carneiro
|
d875f43b52
|
chore: remove outdated TODO
|
2022-08-26 15:31:13 -07:00 |
|
Mario Carneiro
|
ee22e637cd
|
fix: use withContext at ac_rfl
|
2022-08-26 15:23:24 -07:00 |
|
E.W.Ayers
|
ff792c3a3a
|
feat: abstract visitLet, visitLambda, visitForall
|
2022-08-25 19:09:16 -07:00 |
|