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

test(tests/lua): add simple tactic framework test

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-27 18:51:55 -07:00
parent e408998e06
commit 9fb8fd0e7b
1 changed files with 18 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
tests/lua/tactic1.lua Normal file
View file

@ -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