2 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/output/Binder.out b/test-suite/output/Binder.out
new file mode 100644
index 0000000000..34558e9a6b
--- /dev/null
+++ b/test-suite/output/Binder.out
@@ -0,0 +1,8 @@
+foo = fun '(x, y) => x + y
+     : nat * nat -> nat
+forall '(a, b), a /\ b
+     : Prop
+foo = λ '(x, y), x + y
+     : nat * nat → nat
+∀ '(a, b), a ∧ b
+     : Prop
diff --git a/test-suite/output/Binder.v b/test-suite/output/Binder.v
new file mode 100644
index 0000000000..9aced9f665
--- /dev/null
+++ b/test-suite/output/Binder.v
@@ -0,0 +1,7 @@
+Definition foo '(x,y) := x + y.
+Print foo.
+Check forall '(a,b), a /\ b.
+
+Require Import Utf8.
+Print foo.
+Check forall '(a,b), a /\ b.