diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /test-suite/output/PatternsInBinders.out | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'test-suite/output/PatternsInBinders.out')
-rw-r--r-- | test-suite/output/PatternsInBinders.out | 39 |
1 files changed, 39 insertions, 0 deletions
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 |