Patterns in binders: printing tests

1 files changed, 31 insertions, 0 deletions

diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
new file mode 100644
index 000000000..6a28475d7
--- /dev/null
+++ b/test-suite/output/PatternsInBinders.out
@@ -0,0 +1,31 @@
+swap = fun '(x, y) => (y, x)
+     : A * B -> B * A
+fun '(x, y) => (y, x)
+     : A * B -> B * A
+forall '(x, y), swap (x, y) = (y, x)
+     : Prop
+proj_informative = fun 'exist _ x _ => x : A
+     : {x : A | P x} -> A
+foo = fun 'Bar n b tt p => if b then n + p else n - p
+     : Foo -> nat
+baz = 
+fun 'Bar n1 _ tt p1 => fun 'Bar _ _ tt _ => n1 + p1
+     : Foo -> Foo -> nat
+λ '(x, y), (y, x)
+     : A * B → B * A
+∀ '(x, y), swap (x, y) = (y, x)
+     : Prop
+swap = 
+fun (A B : Type) (pat : A * B) => let '(x, y) := pat in (y, x)
+     : forall A B : Type, A * B -> B * A
+
+Arguments A, B are implicit and maximally inserted
+Argument scopes are [type_scope type_scope _]
+forall (A B : Type) (pat : A * B), let '(x, y) := pat in swap (x, y) = (y, x)
+     : Prop
+exists pat : A * A, let '(x, y) := pat in swap (x, y) = (y, x)
+     : Prop
+both_z = 
+fun pat : nat * nat =>
+let '(n, p) as pat0 := pat return (F pat0) in (Z n, Z p) : F (n, p)
+     : forall pat : nat * nat, F pat