29 lines
1.5 KiB
Lua
29 lines
1.5 KiB
Lua
|
assert(level():is_zero())
|
||
|
|
assert(mk_level_zero():is_zero())
|
||
|
|
assert(mk_level_one():is_succ())
|
||
|
|
assert(not mk_level_one():is_zero())
|
||
|
|
assert(mk_level_max(mk_level_zero(), mk_level_one()):is_succ())
|
||
|
|
assert(mk_level_max(mk_param_univ("a"), mk_param_univ("b")):is_max())
|
||
|
|
assert(mk_level_max(mk_level_one(), mk_level_zero()):is_succ())
|
||
|
|
assert(level():succ():is_succ())
|
||
|
|
assert(mk_level_imax(mk_level_one(), mk_level_zero()):is_zero())
|
||
|
|
assert(is_level(mk_level_one()))
|
||
|
|
assert(not is_level(1))
|
||
|
|
assert(mk_level_one():succ_of() == mk_level_zero())
|
||
|
|
assert(mk_level_one():succ_of():is_zero())
|
||
|
|
assert(mk_level_succ(mk_level_succ(level())):is_not_zero())
|
||
|
|
assert(not mk_param_univ("a"):is_not_zero())
|
||
|
|
assert(mk_level_max(mk_param_univ("a"), mk_param_univ("b")):lhs() == mk_param_univ("a"))
|
||
|
|
assert(mk_level_max(mk_param_univ("a"), mk_param_univ("b")):rhs() == mk_param_univ("b"))
|
||
|
|
assert(mk_level_imax(mk_param_univ("a"), mk_param_univ("b")):lhs() == mk_param_univ("a"))
|
||
|
|
assert(mk_level_imax(mk_param_univ("a"), mk_param_univ("b")):rhs() == mk_param_univ("b"))
|
||
|
|
assert(mk_param_univ("a"):id() == name("a"))
|
||
|
|
assert(mk_meta_univ("b"):id() == name("b"))
|
||
|
|
assert(level():trivially_leq(mk_level_one()))
|
||
|
|
assert(level():trivially_leq(mk_param_univ("a")))
|
||
|
|
assert(not mk_param_univ("b"):trivially_leq(mk_param_univ("a")))
|
||
|
|
assert(mk_level_one():kind() == level_kind.Succ)
|
||
|
|
assert(not mk_level_one():has_meta())
|
||
|
|
assert(not mk_level_succ(mk_param_univ("a")):has_meta())
|
||
|
|
assert(mk_level_succ(mk_meta_univ("a")):has_meta())
|