From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 test-suite/output/PatternsInBinders.out | 39 +++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 test-suite/output/PatternsInBinders.out

(limited to 'test-suite/output/PatternsInBinders.out')

diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
new file mode 100644
index 00000000..c012a86b
--- /dev/null
+++ b/test-suite/output/PatternsInBinders.out
@@ -0,0 +1,39 @@
+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) '(Bar _ _ tt _) => n1 + p1
+     : Foo -> Foo -> nat
+swap = 
+fun (A B : Type) '(x, y) => (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 _]
+fun (A B : Type) '(x, y) => swap (x, y) = (y, x)
+     : forall A B : Type, A * B -> Prop
+forall (A B : Type) '(x, y), swap (x, y) = (y, x)
+     : Prop
+exists '(x, y), swap (x, y) = (y, x)
+     : Prop
+exists '(x, y) '(z, w), swap (x, y) = (z, w)
+     : Prop
+λ '(x, y), (y, x)
+     : A * B → B * A
+∀ '(x, y), 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
+fun '(x, y) '(z, t) => swap (x, y) = (z, t)
+     : A * B -> B * A -> Prop
+forall '(x, y) '(z, t), swap (x, y) = (z, t)
+     : Prop
-- 
cgit v1.2.3