diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-11 13:52:58 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-11 13:52:58 +0200 |
| commit | 8e6d03830e9c53f641626e29886eb07c705f7608 (patch) | |
| tree | 43930295d880224ced9e465b6cf2070c916db31c /test-suite | |
| parent | b75d7f21a49bb7c2b7684a06ad3fae89b99e7a94 (diff) | |
| parent | f24d8876837e2f9121064f496d89803f60ec2c71 (diff) | |
Merge PR#594: An example showing the benefit of Econstr
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/unification.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v index 296686e16..6f7498d65 100644 --- a/test-suite/success/unification.v +++ b/test-suite/success/unification.v @@ -188,3 +188,14 @@ Proof. apply idpath. apply idpath. Defined. + +(* An example where it is necessary to evar-normalize the instance of + an evar to evaluate if it is a pattern *) + +Check + let a := ?[P] in + fun (H : forall y (P : nat -> Prop), y = 0 -> P y) + x (p:x=0) => + H ?[y] a p : x = 0. +(* We have to solve "?P ?y[x] == x = 0" knowing from + "p : (x=0) == (?y[x] = 0)" that "?y := x" *) |