diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /test-suite/output/PatternsInBinders.out | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'test-suite/output/PatternsInBinders.out')
-rw-r--r-- | test-suite/output/PatternsInBinders.out | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index c012a86b..8a6d94c7 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -31,9 +31,17 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w) : Prop both_z = fun pat : nat * nat => -let '(n, p) as pat0 := pat return (F pat0) in (Z n, Z p) : F (n, p) +let '(n, p) as x := pat return (F x) 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 +fun (pat : nat) '(x, y) => x + y = pat + : nat -> nat * nat -> Prop +f = fun x : nat => x + x + : nat -> nat + +Argument scope is [nat_scope] +fun x : nat => x + x + : nat -> nat |