Leonardo de Moura
|
af5854ad39
|
doc(examples/lean): use new Import command in examples
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-12-28 12:08:08 -08:00 |
|
Leonardo de Moura
|
f18360a294
|
doc(examples/lean/set): prove antisymmetry for subset relation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-12-26 22:37:44 -08:00 |
|
Leonardo de Moura
|
7eaade4ceb
|
chore(examples/lean): rename examples
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-12-26 16:00:42 -08:00 |
|
Leonardo de Moura
|
f1b97b18b4
|
refactor(frontends/lean/parser): tactic macros, and tactic Lua bindings
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-12-26 15:54:53 -08:00 |
|
Leonardo de Moura
|
b5d23619cb
|
feat(util/script_state): add 'import' command to Lua, it import files from the LEAN_PATH
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-12-22 21:27:12 -08:00 |
|
Leonardo de Moura
|
df58eb132e
|
feat(frontends/lean): simplify explicit version names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-12-21 17:05:25 -08:00 |
|
Leonardo de Moura
|
3eb4de6760
|
fix(frontends/lean/parser): fix deadlock in macro parser
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-12-19 21:40:00 -08:00 |
|
Leonardo de Moura
|
9b14744405
|
chore(examples/lean): use the same notation in the example set.lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-12-18 21:24:04 -08:00 |
|
Leonardo de Moura
|
dd72269b13
|
feat(frontends/lean): rename command Set to SetOption
It is not nice to have Set as a reserved keyword. See example examples/lean/set.lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-12-18 21:18:48 -08:00 |
|
Leonardo de Moura
|
d7886c4f5f
|
doc(examples/lean): new example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-12-18 21:03:16 -08:00 |
|
Leonardo de Moura
|
8cfe5cf9ed
|
fix(frontends/lean/pp): pretty printer was ignoring notation decls in the local scope
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-12-18 18:00:37 -08:00 |
|
Leonardo de Moura
|
79fa6e4940
|
feat(frontends/lean): Scopes in the default Lean frontend
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-12-18 17:40:21 -08:00 |
|
Leonardo de Moura
|
b887a2b900
|
fix(examples/lean/tactic_in_lua): try to make sure the example works when using LuaJIT
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-12-17 08:58:06 -08:00 |
|
Leonardo de Moura
|
caea19dcf0
|
doc(examples/lean): new tactic example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-12-06 16:34:59 -08:00 |
|
Leonardo de Moura
|
4e4fea1eca
|
fix(examples/lean): add all examples to test suite
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-12-05 21:54:55 -08:00 |
|
Leonardo de Moura
|
a7027a1d00
|
feat(library/tactic): polish tactic API, and add new example showing how to implement tactics using Lua
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-11-30 00:16:39 -08:00 |
|
Leonardo de Moura
|
0680865689
|
Fix typo
|
2013-09-05 19:18:55 -07:00 |
|
Leonardo de Moura
|
71d76a891c
|
Add proof by evaluation examples
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-05 18:56:33 -07:00 |
|
Leonardo de Moura
|
9f34f96b08
|
Add another example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-04 05:40:28 -07:00 |
|
Leonardo de Moura
|
0c071d43af
|
Move examples to lean examples subdir. We should have an example subdirectory for each frontend
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-03 20:42:20 -07:00 |
|