michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(lua/justification): add more tests

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-17 11:13:10 -08:00
parent d0bac61e74
commit f586e58ac3
2 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/bindings/lua/leanlua_state.cpp
View file

@ -24,6 +24,7 @@ Author: Leonardo de Moura
#include "bindings/lua/options.h"
#include "bindings/lua/sexpr.h"
#include "bindings/lua/format.h"
#include "bindings/lua/formatter.h"
#include "bindings/lua/level.h"
#include "bindings/lua/local_context.h"
#include "bindings/lua/expr.h"
@ -173,6 +174,7 @@ struct leanlua_state::imp {
open_options(m_state);
open_sexpr(m_state);
open_format(m_state);
open_formatter(m_state);
open_level(m_state);
open_local_context(m_state);
open_expr(m_state);

11
tests/lua/jst1.lua Normal file
View file

@ -0,0 +1,11 @@
local j1 = mk_assumption_justification(1)
local j2 = mk_assumption_justification(2)
assert(is_justification(j1))
assert(j1:depends_on(j1))
assert(not j1:depends_on(j2))
for c in j1:children() do
assert(false)
end
assert(not j2:has_children())
print(j1)
assert(j1:get_main_expr():is_null())