Leonardo de Moura
|
f5741af39d
|
test: minimal repro for Borrow.lean bug
|
2019-12-22 19:16:23 -08:00 |
|
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
|
7490c34b54
|
chore: fix tests
- Delayed assignments do not become regular assignments anymore.
- We can instantiate mvas more aggressively in the new design.
|
2019-12-21 16:03:44 -08:00 |
|
Leonardo de Moura
|
a32fd2e693
|
feat: implement design documented at 868a217202
|
2019-12-21 15:53:36 -08:00 |
|
Leonardo de Moura
|
fdfff29bb1
|
feat: expose liftLooseBVars and lowerLooseBVars
|
2019-12-21 08:57:11 -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
|
d2d6e85719
|
feat: add forRevM
|
2019-12-19 17:24:29 -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
|
f04f51a295
|
test: pattern confusion example
cc @dselsam
|
2019-12-19 13:36:22 -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
|
c5c158e5b9
|
fix: isDefEqQuick
|
2019-12-19 11:10:58 -08:00 |
|
Leonardo de Moura
|
5629870ab0
|
test: news tests
|
2019-12-19 05:51:04 -08:00 |
|
Sebastian Ullrich
|
88a924b728
|
feat: support (almost) proper name resolution in quotations in the old frontend
|
2019-12-18 20:11:45 -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 |
|
Sebastian Ullrich
|
b479015234
|
test: more quotation tests
|
2019-12-18 13:41:39 +01:00 |
|
Leonardo de Moura
|
f49e1ae159
|
chore: fix test
|
2019-12-17 15:34:52 -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 |
|
Sebastian Ullrich
|
5de274781b
|
refactor: remove broken support for nested antiquotations
|
2019-12-17 12:16:34 -08:00 |
|
Sebastian Ullrich
|
de091d1eef
|
feat: use addMacroScope in syntax quotation terms
|
2019-12-17 12:16:34 -08:00 |
|
Sebastian Ullrich
|
76eb7ad205
|
feat: handle nested quotation-antiquotations
|
2019-12-17 12:16:34 -08:00 |
|
Sebastian Ullrich
|
b70edfaa2d
|
test: simple quotation terms
|
2019-12-17 12:16:13 -08:00 |
|
Leonardo de Moura
|
3d6146756f
|
feat: elaborate lambda abstractions
|
2019-12-17 11:44:40 -08:00 |
|
Leonardo de Moura
|
65edd6e37c
|
chore: fix tests
|
2019-12-17 07:37:58 -08:00 |
|
Leonardo de Moura
|
1b9fb2f726
|
fix: elabNum
|
2019-12-16 17:51:29 -08:00 |
|
Leonardo de Moura
|
9838a6a8b1
|
chore: fix tests
|
2019-12-16 10:31:51 -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
|
a1aac9a98d
|
chore: fix tests
|
2019-12-15 18:34:13 -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
|
32cebc3e76
|
feat: add getBaseStructurePath
|
2019-12-14 13:11:22 -08:00 |
|
Leonardo de Moura
|
54e5ca0c7b
|
fix: lean_nat_abs
It must not assume a nonnegative big integer is a big nat.
|
2019-12-14 08:08:41 -08:00 |
|
Leonardo de Moura
|
869b133b59
|
chore: fix tests
|
2019-12-13 19:25:35 -08:00 |
|
Leonardo de Moura
|
119742e463
|
feat: make sure MetaM also implements new unifier approximation
|
2019-12-13 19:12:53 -08:00 |
|
Leonardo de Moura
|
cac78d7e88
|
test: add new test
|
2019-12-13 18:27:23 -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
|
d18e8d95b9
|
feat: add isStructure
|
2019-12-12 08:48:49 -08:00 |
|