Leonardo de Moura
|
d4aa99969f
|
chore: update stage0
|
2020-08-27 12:08:32 -07:00 |
|
Leonardo de Moura
|
90bddeb12b
|
feat: add lean_task_get_own for implementing Task.get
|
2020-08-27 12:07:11 -07:00 |
|
Leonardo de Moura
|
c4f38c08b2
|
feat: collectMVars methods
|
2020-08-27 11:24:03 -07:00 |
|
Leonardo de Moura
|
5349a73655
|
chore: add MessageData.nestD
"default nest"
|
2020-08-27 11:22:47 -07:00 |
|
Leonardo de Moura
|
99161538f8
|
feat: add Declaration.forExprM and Declaration.foldExprM
|
2020-08-27 11:22:11 -07:00 |
|
Leonardo de Moura
|
bb3c8a2105
|
refactor: polymorphic applyAttributes
|
2020-08-27 10:46:33 -07:00 |
|
Leonardo de Moura
|
d84078283c
|
chore: helper method
|
2020-08-27 09:52:33 -07:00 |
|
Leonardo de Moura
|
4495c13e6c
|
fix: extra line
|
2020-08-27 09:11:04 -07:00 |
|
Leonardo de Moura
|
ed976027fe
|
chore: naming convention
|
2020-08-26 20:24:33 -07:00 |
|
Leonardo de Moura
|
09a375b540
|
feat: reject _ where function is expected
It should behave like Lean3.
|
2020-08-26 18:48:05 -07:00 |
|
Leonardo de Moura
|
4934a2d522
|
chore: remove workaround
|
2020-08-26 16:24:20 -07:00 |
|
Leonardo de Moura
|
7db6f420f5
|
refactor: move mkAuxDefinitionCore
|
2020-08-26 16:20:09 -07:00 |
|
Leonardo de Moura
|
011d8c02c8
|
test: letrec error messages
|
2020-08-26 15:30:19 -07:00 |
|
Leonardo de Moura
|
00599cf62b
|
fix: types of the recursive functions being defined cannot reference other functions in the same mutual block
|
2020-08-26 15:29:06 -07:00 |
|
Leonardo de Moura
|
8543a20b8f
|
feat: add checkpoint using withSynthesize
|
2020-08-26 15:10:26 -07:00 |
|
Leonardo de Moura
|
89bd5d6da2
|
fix: bug introduced today
|
2020-08-26 14:49:20 -07:00 |
|
Leonardo de Moura
|
5d036d0ca3
|
feat: generalize mkClosure
|
2020-08-26 14:45:46 -07:00 |
|
Leonardo de Moura
|
5af763f243
|
feat: use checkNotAlreadyDeclared
|
2020-08-26 13:44:25 -07:00 |
|
Leonardo de Moura
|
de2df5955f
|
refactor: polymorphic checkNotAlreadyDeclared
|
2020-08-26 13:42:57 -07:00 |
|
Leonardo de Moura
|
497d8592cf
|
feat: elaborate letrec values
|
2020-08-26 13:35:51 -07:00 |
|
Leonardo de Moura
|
1f2204af96
|
feat: add LetIdDeclView
|
2020-08-26 13:28:41 -07:00 |
|
Leonardo de Moura
|
f4f0684636
|
chore: remove dead code
|
2020-08-26 13:19:13 -07:00 |
|
Leonardo de Moura
|
5dc5e8a92f
|
feat: add LetRecView and expand letEqnsDecl occurring in letrec's
|
2020-08-26 11:30:06 -07:00 |
|
Leonardo de Moura
|
546c108497
|
chore: revise letrec syntax
|
2020-08-26 10:50:32 -07:00 |
|
Leonardo de Moura
|
70e508d704
|
chore: add Lean/Elab/LetRec.lean
|
2020-08-26 10:07:59 -07:00 |
|
Leonardo de Moura
|
ee46a9e360
|
chore: update stage0
|
2020-08-26 09:58:39 -07:00 |
|
Leonardo de Moura
|
effaf64a07
|
feat: allow user to specify attributes letrec declarations
|
2020-08-26 09:57:46 -07:00 |
|
Leonardo de Moura
|
8a9b031a9d
|
refactor: add Lean/Elab/Attributes.lean
|
2020-08-26 09:54:48 -07:00 |
|
Leonardo de Moura
|
a413da856f
|
refactor: polymorphic elabAttrs and elabAttr
|
2020-08-26 09:50:03 -07:00 |
|
Leonardo de Moura
|
524eca4d7f
|
chore: udpate stage0
|
2020-08-26 09:39:01 -07:00 |
|
Leonardo de Moura
|
d129d93dde
|
chore: add letrec to the list of keywords
|
2020-08-26 09:37:50 -07:00 |
|
Leonardo de Moura
|
6a83577703
|
feat: letrec syntax
|
2020-08-26 09:33:52 -07:00 |
|
Leonardo de Moura
|
5a7bf86a42
|
test: add test for buggy compiler step
Bug was fixed at da928f8c0
|
2020-08-26 08:34:35 -07:00 |
|
Leonardo de Moura
|
6683a85414
|
chore: update stage0
|
2020-08-26 08:34:35 -07:00 |
|
Leonardo de Moura
|
467e912380
|
fix: bug on JP handling
|
2020-08-26 08:34:35 -07:00 |
|
Leonardo de Moura
|
76f9b155a1
|
chore: document kind of crash
|
2020-08-26 08:34:35 -07:00 |
|
Leonardo de Moura
|
5efa628e43
|
chore: split Lift.lean into MonadLift.lean, MonadFunctor.lean, and MonadRun.lean
|
2020-08-26 08:34:35 -07:00 |
|
Sebastian Ullrich
|
2c1b0e3114
|
chore: remove hanging stdlib bench test from CI
|
2020-08-26 11:34:43 +02:00 |
|
Leonardo de Moura
|
321719b300
|
feat: add MonadFinally
|
2020-08-25 17:58:35 -07:00 |
|
Leonardo de Moura
|
31716731ba
|
chore: cleanup
|
2020-08-25 15:06:12 -07:00 |
|
Leonardo de Moura
|
48851705b6
|
chore: update stage0
|
2020-08-25 14:59:08 -07:00 |
|
Leonardo de Moura
|
813a964767
|
refactor: move polymorphic Meta methods back to Meta namespace
|
2020-08-25 14:57:58 -07:00 |
|
Leonardo de Moura
|
cf0149a1a7
|
refactor: use MonadControlT
|
2020-08-25 13:54:42 -07:00 |
|
Leonardo de Moura
|
7888919aa9
|
test: MonadControl
|
2020-08-25 13:54:41 -07:00 |
|
Leonardo de Moura
|
b095f0652a
|
fix: tryLiftAndCoe
|
2020-08-25 13:54:41 -07:00 |
|
Leonardo de Moura
|
1103806ff4
|
refactor: HasMonadLift ==> MonadLift
|
2020-08-25 13:54:41 -07:00 |
|
Leonardo de Moura
|
b03cd748cf
|
feat: add MonadControl
|
2020-08-25 13:54:41 -07:00 |
|
Sebastian Ullrich
|
589afc4095
|
doc: wording
|
2020-08-25 16:12:19 +02:00 |
|
mhuisi
|
21d176c1ea
|
doc: correct msys2 build instructions
|
2020-08-25 16:08:58 +02:00 |
|
Leonardo de Moura
|
e5b7daf9c2
|
refactor: make AppBuilder methods polymorphic
|
2020-08-24 18:23:34 -07:00 |
|