test(lua): add coercion sort-class tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
e28446710e
commit
0d02f933cb
1 changed files with 13 additions and 0 deletions
13
tests/lua/coe3.lua
Normal file
13
tests/lua/coe3.lua
Normal file
|
@ -0,0 +1,13 @@
|
|||
local env = environment()
|
||||
local l = param_univ("l")
|
||||
env = add_decl(env, mk_var_decl("group", {l}, mk_sort(l+1)))
|
||||
env = add_decl(env, mk_var_decl("abelian_group", {l}, mk_sort(l+1)))
|
||||
local group = Const("group", {l})
|
||||
local ab_group = Const("abelian_group", {l})
|
||||
env = add_decl(env, mk_var_decl("carrier", {l}, mk_arrow(group, mk_sort(l))))
|
||||
env = add_coercion(env, "carrier")
|
||||
env = add_decl(env, mk_var_decl("abg2g", {l}, mk_arrow(ab_group, group)))
|
||||
env = add_coercion(env, "abg2g")
|
||||
for_each_coercion_sort(env, function(C, f) print(tostring(C) .. " >-> sort : " .. tostring(f)) end)
|
||||
print(get_coercion_to_sort(env, Const("abelian_group", {1})))
|
||||
assert(env:type_check(get_coercion_to_sort(env, Const("abelian_group", {1}))))
|
Loading…
Reference in a new issue