diff options
| author | Maxime Dénès | 2020-03-31 10:17:02 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-03-31 10:17:02 +0200 |
| commit | ea8c40c17c7301158365dde13d3ceeeeffa6c063 (patch) | |
| tree | 8344c297a8cba0711983c07e6b5e64c7fa659f51 /test-suite | |
| parent | e2f0814688511be93659c2258b91248698f18d4a (diff) | |
| parent | 830cdec8704d14bca0b3db390ecb9661e01eb106 (diff) | |
Merge PR #11668: Helping issue #11659 by leaving only the Cast hack in the grammar.
Reviewed-by: ejgallego
Reviewed-by: maximedenes
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/PatternsInBinders.out | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index 4f09f00c56..bdfa8afb6a 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -4,7 +4,7 @@ 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 +proj_informative = fun '(exist _ x _) => x : {x : A | P x} -> A foo = fun '(Bar n b tt p) => if b then n + p else n - p : Foo -> nat @@ -29,8 +29,7 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w) ∀ '(x, y), swap (x, y) = (y, x) : Prop both_z = -fun pat : nat * nat => -let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p) +fun pat : nat * nat => let '(n, p) as x := pat return (F x) in (Z n, Z p) : forall pat : nat * nat, F pat fun '(x, y) '(z, t) => swap (x, y) = (z, t) : A * B -> B * A -> Prop |