Leonardo de Moura
|
b633c866e6
|
Expose environment API in the frontend object. Add support for formatting objects.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-17 10:55:42 -07:00 |
|
Leonardo de Moura
|
111cdd4e62
|
Remove pretty printer from kernel. Add basic printing capability to exprlib module.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-16 20:40:39 -07:00 |
|
Leonardo de Moura
|
519a290f32
|
Refactor kernel objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-16 20:40:39 -07:00 |
|
Leonardo de Moura
|
c41b3dc4d8
|
Add kernel_exceptions. The idea is to avoid expression formatting in the kernel. It also allows different frontends to display the error messages is a different way.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-16 12:51:12 -07:00 |
|
Leonardo de Moura
|
013fa866fa
|
Add iterator for traversing local objects (i.e., ignores objects defined in ancestor environments)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-15 19:02:28 -07:00 |
|
Leonardo de Moura
|
2b7834c5fc
|
Add methods for creating infix, prefix, postfix operators in the frontend object
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-15 19:02:28 -07:00 |
|
Leonardo de Moura
|
b0f2ee6de0
|
Add notation support to frontend object
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-14 18:17:18 -07:00 |
|
Leonardo de Moura
|
392b347f53
|
Add expr_formatter and expr_locator. Add better error messages. Improve simple printer.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-13 19:16:40 -07:00 |
|
Leonardo de Moura
|
11a9cac5d6
|
Refactor kernel objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-13 15:13:54 -07:00 |
|
Leonardo de Moura
|
9fbe99bf58
|
Rename define_uv -> add_uvar
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-10 14:21:13 -07:00 |
|
Leonardo de Moura
|
3d9f9a12d1
|
Enable automatic coercion from 'char const *' to hierachical name
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-10 14:21:13 -07:00 |
|
Leonardo de Moura
|
ecf9506abe
|
Add object iterator for environment objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-08 18:38:18 -07:00 |
|
Leonardo de Moura
|
2670e94398
|
Add pretty printer for Lean environment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-07 19:10:12 -07:00 |
|
Leonardo de Moura
|
ab915fb3f0
|
Add add_theorem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-06 12:24:20 -07:00 |
|
Leonardo de Moura
|
33d2dd2d8b
|
Add subst proof rule. Define symm and trans using subst.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-06 02:03:22 -07:00 |
|
Leonardo de Moura
|
30513398bb
|
Add basic definitions and axioms
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-05 20:06:42 -07:00 |
|
Leonardo de Moura
|
70de591934
|
Add definitions and facts
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-04 20:52:14 -07:00 |
|
Leonardo de Moura
|
5f77a2367f
|
Allow Boolean expressions (aka propositions) to be used as types.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-04 18:26:01 -07:00 |
|
Leonardo de Moura
|
4b5d60f2b2
|
Add get_uvar method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-04 17:47:54 -07:00 |
|
Leonardo de Moura
|
c97db1f0cf
|
Add children environments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-04 16:07:37 -07:00 |
|
Leonardo de Moura
|
6452c69b96
|
Use level at kernel expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-07-29 19:44:26 -07:00 |
|
Leonardo de Moura
|
537e2c101c
|
Add more tests. Fix bug in universe implication test.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-07-29 19:05:43 -07:00 |
|
Leonardo de Moura
|
a4f456c99e
|
Universe levels
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-07-28 22:34:39 -07:00 |
|