coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Randy Pollack <rpollack0 AT gmail.com>
- To: Coq-Club Club <coq-club AT inria.fr>
- Subject: [Coq-Club] "Unable to unify"
- Date: Wed, 14 Dec 2016 17:17:47 +0000
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=rpollack0 AT gmail.com; spf=Pass smtp.mailfrom=rpollack0 AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f47.google.com
- Ironport-phdr: 9a23:9i5t5ha59pjFZhB/V2q/3FH/LSx+4OfEezUN459isYplN5qZpcyzbnLW6fgltlLVR4KTs6sC0LuN9f6+EjBdqdbZ6TZZL8wKD0dEwewt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2ap42N2uuz45zeZRlTzHr4OOsqbUb+kQKEnc4PxKBmN6x54R/UqDMccONPgGhsOFi7nhDm58728oQ1oApKvPd0zcdGXbSyR6M8SbVTD3xyKXgy4MnivhqbZQSK73oYFG4Rl0wbUED+8BjmU8Kp4WPBve1n1XzfZJWuQA==
Coq says:
Unable to unify "?z@{z:=(z0, z1, z2)}" with "(z0, strips z1, z2)"
(cannot instantiate "?z" because "z0" is not in its scope: available
arguments are "p" "dts" "m" "(z0, z1, z2)" "fn" "arg"
"s" "x" "t" "t'" "args" "fsts" "lsts" "ix" "w" "H"
"e" "e0" "w0" "H0" "e1" "w1" "H1").
This can be solved with a tiny lemma, but it seems unnecessarily
restrictive that (z0,z1,z2) is in the scope of ?z, but z0 is not in
the scope.
--Randy
- [Coq-Club] "Unable to unify", Randy Pollack, 12/14/2016
- Re: [Coq-Club] "Unable to unify", Jason Gross, 12/14/2016
Archive powered by MHonArc 2.6.18.