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
Leonardo de Moura
fc375b56bc
test: Structure.lean
2019-12-12 08:28:57 -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
34332ecaa9
fix: forallBoundedTelescope
2019-12-11 18:08:41 -08:00
Leonardo de Moura
4b285a48dc
fix: forallMetaTelescopeReducing
2019-12-11 18:03:11 -08:00
Leonardo de Moura
77bf2a60e1
fix: lambdaMetaTelescope
2019-12-11 17:50:34 -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
7da9793c0a
chore: fix tests
2019-12-09 16:58:21 -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
1352619ee4
refactor: MonadTracer and helper functions
...
This commit adds
- `addContext : MessageData -> m MessageData` method. We need it to
make sure we wrap the message with the current context. Before this
commit I had to redefine `trace` for `MetaM`, `SynthM`, and
`TermElabM`.
- polymorphic `traceM` method.
2019-12-08 09:05:15 -08:00
Leonardo de Moura
efaec02b23
feat: add basic commands
2019-12-07 17:55:31 -08:00
Sebastian Ullrich
9482976345
test: speed up some tests for the debug interpreter
2019-12-07 21:51:59 +01:00
Leonardo de Moura
2ae92340ef
feat: add intro and assumption
2019-12-05 10:57:48 -08:00
