coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: Coq-Club Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] "Unable to unify"
- Date: Wed, 14 Dec 2016 18:32:14 +0000
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f181.google.com
- Ironport-phdr: 9a23:nWQXrRY3M20eWoPhuvgcONr/LSx+4OfEezUN459isYplN5qZr8y7bnLW6fgltlLVR4KTs6sC0LuN9f6+EjFZqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjSwbLd8IRmsrAjct8YajIt/Jq0s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlTwKPCAl/m7JlsNwjbpboBO/qBx5347Ue5yeOP5ncq/AYd8WWW9NU8BMXCJDH4y8dZMCAOUPPelar4fzqVgAowagCwawH+7g0CNEi2Xs0KEmz+gsEwfL1xEgEdIUt3TUqc34OqMIXuCuy6nIyyjIYfJM2Tf684jIaQ0qrPaOXb1qasrRzk8vFwzfjlWXsozlJDeY2/8Cs2ie9eVgVOavh3Q7pAF2pzii38EhgZTHiIISz1DL7yR5wIAtKN25Tk57e9+kH4FKuyGULYt7RN4pTWJwuCsi1LEKpZq2cDIJxZkn3RLTdeKLf5SS7h7+V+udPDF1j29/dr2lnRa9602gx/X8Vsaq1FZKqTJIktzWuXAM0xzf89GHSvhh8ku41zaDygPe5vxeLUA7kqrbLJEhwroumZYJrUvDGSr2lF33jK+QaEok5vCl5/r7brjivJORNI95hhvgPqgwhsCzG/k0PwsTU2SD/OSzzrzj/Un3QLVQif02l7HUsJLAKsQAoa65BQBV0pwk6xakFDer1M8VnXYCLF1feRKHi5LlNE3JIPD9Ffu/mUijkC93x/DaOb3sGonCLn/akLv4Ybl971NcxxEowNBE55NUD6kBL+jpVk/wstzYFB45PBauz+bpEtUunr8ZDEmIG+qyNL7Y+XSM++hnd+KLfcoevCv3A/kj/f/ny3EjzwwzZ66siLkec3e+Vtt8JF6CKS7ui8wGF2gQuRElHcTljVSDVXhYYHPkDPF03S0yFI/zVdSLfYuqmrHUmX7jRpA=
I've made https://coq.inria.fr/bugs/show_bug.cgi?id=5264 for this (it was previously mentioned in a few other bugs, but I think it deserves its own report)
On Wed, Dec 14, 2016, 12:18 PM Randy Pollack <rpollack0 AT gmail.com> wrote:
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.