lean2/tests/lua/unify3.lua

local env     = environment()
local group   = Const("group")
local carrier = Const("carrier")
local real    = Const("real")
local nat     = Const("nat")
env = add_decl(env, mk_var_decl("group", mk_sort(2)))
env = add_decl(env, mk_var_decl("carrier", mk_arrow(group, Type)))
env = add_decl(env, mk_var_decl("real", Type))
env = add_decl(env, mk_var_decl("nat",  Type))
env = add_decl(env, mk_var_decl("real_group", group))
env = add_decl(env, mk_var_decl("nat_group", group))
local real_group = Const("real_group")
local nat_group  = Const("nat_group")
local m = mk_metavar("m", mk_metavar("m_ty", mk_sort(mk_meta_univ("u"))))
local cs  = { mk_eq_cnstr(carrier(m), real) }
assert(not unify(env, cs, name_generator())())