diff --git a/tests/lua/expr8.lua b/tests/lua/expr8.lua new file mode 100644 index 000000000..c7252cb61 --- /dev/null +++ b/tests/lua/expr8.lua @@ -0,0 +1,9 @@ +local Or = Const("or") +local A = Local("A", Type) +local a = Local("a", A) +local b = Local("b", A) +local H = Local("H", Or(a, b)) +print(Pi({A, {a, true}, {b, Bool}, {H, binder_info(false, true)}}, Or(b, a))) +print(Pi({A, a, b, H}, Or(b, a))) +print(Fun({A, {a, true}, {b, Bool}, {H, binder_info(false, true)}}, Or(b, a))) +print(Fun({A, a, b, H}, Or(b, a)))