coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Generalizing binders don't seem to work as described

From: Karl Crary <crary AT cs.cmu.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Generalizing binders don't seem to work as described
Date: Fri, 30 Mar 2018 10:45:17 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=crary AT cs.cmu.edu; spf=Pass smtp.mailfrom=crary AT andrew.cmu.edu; spf=None smtp.helo=postmaster AT mail-qk0-f182.google.com
Ironport-phdr: 9a23:OK+x/xVdllORM0yCtzS0NXY6R5HV8LGtZVwlr6E/grcLSJyIuqrYYxSAt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/JisJ+kaFVrhyvqBNw34Hab5qYNOZ8c67HYd8WWWRMU8RXWidcAo28dYwPD+8ZMOhdtYb9vV8OpgagCAm2Huzv0D9JjWLx0KImyeQuCxvG3Qw7Et0Sq3TYtsn6NKIPUeyv0qbH0CjDYupQ1Dzg64bIaggsre+QUb90a8bcykkiGxnbglmOtYDpJS6Z2+cTv2SD8uZsSf6jh3Qmpg1rrTWixd0ghpTGi48UzF3P6D93z5wvJdKiTU52ed6kH4VUtyGdL4Z2R9ktQ2BsuCoj070GuoK3cDEEyJg6xBPTdeaLc4eP4hLkW+aRJSl3iGh5d7K4gha+6UmgyuviWcmoyFtGsDZJn93Wun0O1xHf8NaLRuVh8ku7xDqC1B7f5vlBIU8ulKrbL5AhwqQ3lpoWqUnMAjX2l1/sjK6WbUgr4O6o5Pn9Yrr4qJ6QLZN7igTjMqg0hMOwHPk4PhAUX2eH4eS8yKHj/UrhTbpWif02i7DVv4zeJcQGvaG0GBRV04Ym6xanFTiqytUYnX8dLFJEYh2LlYbpO0udaMz/WPy4mhGnlCph7/HAJLzoRJvXfVbZl7K0Xr9n7wZ30gMp3JgL7IhdEKApK+m1UUrs8tHUE0lqYESP3+/7BYAlhcslUmWVD/rBafKAgRqz/usqZtK0SsoQsTf5JeIi4qew33Y/lUUQYu+i2IZRZXylTK0/fxepJEH0i9JEKl8k+xIkRbWw2laZFzVWejC/U79uvmhmWrLjNp/KQ8WWuJLE3Cq/GccINGVPC1TJCHSwMovdC61KZyWVLcts1DcDUOr5Rg==

I'm puzzled by the behavior of generalizing binders. This is code from Coq manual:

Class EqDec (A : Type) :=
{ eqb : A -> A -> bool ;
eqb_leibniz : forall x y, eqb x y = true -> x = y }.

Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y).

In regards to the second declaration, the manual says "Here A is implicitly generalized." But this seems not to be the case. I get the error message:

Error: Unbound and ungeneralizable variable A

What am I doing wrong?

-- Karl Crary

[Coq-Club] Generalizing binders don't seem to work as described, Karl Crary, 03/30/2018
- Re: [Coq-Club] Generalizing binders don't seem to work as described, Li-yao Xia, 03/30/2018
- Re: [Coq-Club] Generalizing binders don't seem to work as described, Tej Chajed, 03/30/2018