From 9fb8fd0e7b492d76b413d291d6220ef93ee277a7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 27 Jun 2014 18:51:55 -0700 Subject: [PATCH] test(tests/lua): add simple tactic framework test Signed-off-by: Leonardo de Moura --- tests/lua/tactic1.lua | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 tests/lua/tactic1.lua diff --git a/tests/lua/tactic1.lua b/tests/lua/tactic1.lua new file mode 100644 index 000000000..c7b57dcdb --- /dev/null +++ b/tests/lua/tactic1.lua @@ -0,0 +1,18 @@ +local env = environment() +local A = Local("A", Type) +env = add_decl(env, mk_var_decl("eq", Pi(A, mk_arrow(A, A, Bool)))) +local eq = Const("eq") +local a = Local("a", A) +local b = Local("b", A) +local H = Local("H", eq(A, a, b)) +local m = mk_metavar("m", Pi({A, a, b, H}, eq(A, a, b))) +print(to_proof_state(m)) +local s = to_proof_state(m) +local t = Then(Append(trace_tac("tst1a"), trace_tac("tst1b")), + trace_tac("tst2"), + Append(trace_tac("tst3"), assumption_tac())) +for r in t(env, s) do + print("Solution:") + print(r) + print("---------") +end