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

test(lua): add example for testing is_descendant

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-08 18:50:24 -07:00
parent bc1a91496a
commit 129d108d0b
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lua/env4.lua Normal file
View file

@ -0,0 +1,6 @@
local env = empty_environment()
env = add_decl(env, mk_var_decl("A", Bool))
local c1 = type_check(env, mk_axiom("p", Const("A")))
local c2 = type_check(env, mk_axiom("q", Const("A")))
env = env:add(c1)
env = env:add(c2)