Leonardo de Moura
|
bceb02951c
|
feat: better postpone messages
|
2019-12-22 10:24:22 -08:00 |
|
Leonardo de Moura
|
d53c5a31cb
|
refactor: use PersistentArray to implement MessageLog
Motivation: consistency. Now, Traces and MessageLog use the same datastructure.
|
2019-12-22 08:11:20 -08:00 |
|
Leonardo de Moura
|
a32fd2e693
|
feat: implement design documented at 868a217202
|
2019-12-21 15:53:36 -08:00 |
|
Leonardo de Moura
|
5adadc3158
|
test: document let issue
TODO: fix issue at `Meta.mkLambda` when some of the free variables are let-declarations.
|
2019-12-19 17:29:26 -08:00 |
|
Leonardo de Moura
|
93f4184125
|
feat: elaborate let
|
2019-12-19 17:00:19 -08:00 |
|
Leonardo de Moura
|
8431303999
|
test: new test
|
2019-12-19 14:45:17 -08:00 |
|
Leonardo de Moura
|
bfca7e32e0
|
fix: try to postpone if function type is not known
|
2019-12-19 14:20:56 -08:00 |
|
Leonardo de Moura
|
8d81e89e53
|
feat: elaborate $.
|
2019-12-19 14:16:28 -08:00 |
|
Leonardo de Moura
|
57f6881c6c
|
feat: restore state when catching Exception.postpone
cc @Kha
|
2019-12-19 13:21:11 -08:00 |
|
Leonardo de Moura
|
3e5527219f
|
test: add foldl test
|
2019-12-19 12:06:47 -08:00 |
|
Leonardo de Moura
|
eb24ec56dc
|
feat: add array literal notation
|
2019-12-19 11:42:39 -08:00 |
|
Leonardo de Moura
|
fc5fb07fc3
|
fix: mkFreshExprMVar
|
2019-12-19 11:13:22 -08:00 |
|
Leonardo de Moura
|
6cc928d180
|
test: add postpone test
|
2019-12-18 20:04:38 -08:00 |
|
Leonardo de Moura
|
00cc28096c
|
feat: add support for postponing elabTerm
|
2019-12-18 11:05:02 -08:00 |
|
Leonardo de Moura
|
37b2393479
|
chore: change antiquotation symbol
|
2019-12-17 15:24:12 -08:00 |
|
Leonardo de Moura
|
a1373d68c9
|
fix: fun (_ : A) => ... notation
|
2019-12-17 14:28:48 -08:00 |
|
Leonardo de Moura
|
f6d9f4029e
|
feat: elaborate cdot
|
2019-12-17 13:41:46 -08:00 |
|
Leonardo de Moura
|
1b6319788e
|
feat: elaborate parenSpecial
|
2019-12-17 13:32:46 -08:00 |
|
Leonardo de Moura
|
3d6146756f
|
feat: elaborate lambda abstractions
|
2019-12-17 11:44:40 -08:00 |
|
Leonardo de Moura
|
1b9fb2f726
|
fix: elabNum
|
2019-12-16 17:51:29 -08:00 |
|
Leonardo de Moura
|
c6c68cc4b1
|
feat: elaborate numerals
|
2019-12-16 10:28:28 -08:00 |
|
Leonardo de Moura
|
34b8e3ef04
|
feat: elaborate string literals
|
2019-12-16 10:28:28 -08:00 |
|
Leonardo de Moura
|
356e914ea7
|
feat: elaborate a[i] notation
|
2019-12-15 18:05:53 -08:00 |
|
Leonardo de Moura
|
9d4f2bc4a8
|
fix: break identifier into pieces
|
2019-12-15 08:20:52 -08:00 |
|
Leonardo de Moura
|
e25bd36dc5
|
feat: field projections
|
2019-12-14 13:29:14 -08:00 |
|
Leonardo de Moura
|
41f4476ca8
|
feat: add synthetic sorry
|
2019-12-12 15:18:38 -08:00 |
|
Leonardo de Moura
|
c595eead5c
|
feat: simplify exception handling
|
2019-12-12 14:00:39 -08:00 |
|
Leonardo de Moura
|
36648ebe69
|
fix: DiscrTree.getKeyArgs
|
2019-12-12 05:04:31 -08:00 |
|
Leonardo de Moura
|
d6b4b96ab8
|
test: HasBeq Nat instance
|
2019-12-11 18:09:23 -08:00 |
|
Leonardo de Moura
|
2ae62fd3e8
|
test: instances generated by class command
|
2019-12-11 17:22:55 -08:00 |
|
Leonardo de Moura
|
cb8dacf76a
|
feat: elaborate missing notation
|
2019-12-11 16:41:41 -08:00 |
|
Leonardo de Moura
|
8fd70ee882
|
feat: add builtin notation
|
2019-12-11 16:22:23 -08:00 |
|
Leonardo de Moura
|
a119bdd8e4
|
feat: elaborate instance implicit arguments
|
2019-12-11 15:23:23 -08:00 |
|
Leonardo de Moura
|
becbc9e2eb
|
feat: elaborate $
|
2019-12-11 14:15:24 -08:00 |
|
Leonardo de Moura
|
ef82c327eb
|
fix: List notation
|
2019-12-11 10:49:06 -08:00 |
|
Leonardo de Moura
|
a884280e24
|
feat: elaborate named arguments
|
2019-12-11 09:40:46 -08:00 |
|
Leonardo de Moura
|
e13a10fbf2
|
feat: elaborate explicit and implicit arguments
|
2019-12-11 09:04:26 -08:00 |
|
Leonardo de Moura
|
4f730d82e0
|
feat: elabAppFn
|
2019-12-11 06:19:12 -08:00 |
|
Leonardo de Moura
|
49b7660d38
|
feat: elabApp skeleton
|
2019-12-10 10:21:14 -08:00 |
|
Leonardo de Moura
|
5d11e87fc6
|
feat: elaborate (...)
|
2019-12-09 17:05:40 -08:00 |
|
Leonardo de Moura
|
45c18ad79c
|
chore: make sure we fail test if there are errors
|
2019-12-09 16:55:51 -08:00 |
|
Leonardo de Moura
|
124ad70bfe
|
feat: elaborate dependent arrows
|
2019-12-09 16:49:26 -08:00 |
|
Leonardo de Moura
|
04ff23f81d
|
feat: elaborate arrows
|
2019-12-09 16:31:35 -08:00 |
|
Leonardo de Moura
|
e665960ee9
|
feat: elaborate forall
|
2019-12-09 16:25:53 -08:00 |
|
Leonardo de Moura
|
d586dc6c68
|
feat: add Lean.Elab.process
|
2019-12-09 16:04:49 -08:00 |
|
Leonardo de Moura
|
86c1e97523
|
feat: propagate Options
|
2019-12-09 15:49:47 -08:00 |
|
Leonardo de Moura
|
c7b8a03b14
|
fead: add basic elabId
|
2019-12-08 19:14:44 -08:00 |
|
Leonardo de Moura
|
a15a6967b3
|
feat: add #check command
|
2019-12-08 18:03:34 -08:00 |
|
Leonardo de Moura
|
fddeecaaa6
|
feat: elaborate binders
|
2019-12-08 17:59:11 -08:00 |
|
Leonardo de Moura
|
efaec02b23
|
feat: add basic commands
|
2019-12-07 17:55:31 -08:00 |
|