lean2/tests/lua/expr8.lua

import("util.lua")
local f, g, a, b, c, d = Consts("f, g, a, b, c, d")
local N, M = Consts("N, M")
local x = Var(0)
local y = Var(1)
assert(f(a):closed())
local F = f(g(x, a), f(b, f(x, c)))
assert(F:has_free_vars())
assert(F:has_free_var(0))
assert(not F:has_free_var(1))
assert(F:has_free_var(0, 2))
assert(not F:has_free_var(1, 3))
local c = 0
F:for_each(function() c = c + 1; return false end)
assert(c == 1)
assert(x:is_var())
assert(not x:is_app())
assert(F:is_app())
assert(Let(a, b, f(a)):is_let())
assert(fun(a, N, f(a)):is_lambda())
assert(Pi(a, N, f(a)):is_pi())
assert(Pi(a, N, f(a)):is_abstraction())
assert(fun(a, N, f(a)):is_abstraction())
assert(mk_metavar("M"):is_metavar())
assert(mk_real_value(mpq(10)):is_value())
assert(not F:has_metavar())
assert(f(mk_metavar("M")):has_metavar())
assert(HEq(a, b):is_heq())
assert(F:num_args() == 3)
assert(F:arg(0) == f)
assert(F:arg(1) == g(x, a))
assert(not pcall(function() F:arg(3) end))
assert(not pcall(function() F:arg(-3) end))
local l1 = level(level("N"), 10)
print(l1)
assert(Type(l1):fields() == l1)
assert(a:fields() == name("a"))
assert(y:fields() == 1)
assert(mk_metavar("M"):fields() == name("M"))
assert(a:occurs(F))
assert(F:hash() == F:hash())
assert(a:hash() ~= F:hash())
assert(mk_nat_value(mpz(10)):is_value())
assert(not pcall(function() Var(0):num_args() end))
assert(not pcall(function() print(fun(N, a)) end))