diff options
| author | Hugo Herbelin | 2020-02-23 22:18:24 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-27 14:41:11 +0100 |
| commit | 830cdec8704d14bca0b3db390ecb9661e01eb106 (patch) | |
| tree | e3ff5ae4739551f6cf5f46f5a32aa1776cf77611 /test-suite | |
| parent | bc500cd96c7142cda5ad6f992c7c656d6499b0c6 (diff) | |
Helping issue #11659 by leaving only the Cast hack in the grammar.
We clean the hack bypassing the interpretation of "'pat" in binders
and move it to comDefinition.ml. In particular, we fix the exact
subterm to which Eval has to apply in the hack, and remove the
artificial cast we had introduced.
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 |