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

fix(tests/lua/res1): adjust test to recent modifications

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-20 16:26:41 -08:00
parent 01ce57e52e
commit f2e878dbe7
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
tests/lua/res1.lua
View file

@ -116,8 +116,7 @@ print_types(env, H1, H2, H3, H4, H5, H6, H7)
print(tostring(Pr4) .. " : " .. tostring(tc:check(Pr4))) print(tostring(Pr4) .. " : " .. tostring(tc:check(Pr4)))
print("----------------") print("----------------")
print("Type checking again, but using trust_lvl=0, macros will be expanded during type checking") local env = bare_environment({trust_lvl=1})
local env = bare_environment({trust_lvl=0})
env = init_env(env) env = init_env(env)
env = assert_some_axioms(env) env = assert_some_axioms(env)
local tc = type_checker(env) local tc = type_checker(env)