coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Li-yao Xia <lysxia AT gmail.com>
To: Karl Crary <crary AT cs.cmu.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Generalizing binders don't seem to work as described
Date: Fri, 30 Mar 2018 10:52:48 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=lysxia AT gmail.com; spf=Pass smtp.mailfrom=lysxia AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f180.google.com
Ironport-phdr: 9a23:vsO6uhIksCVTpzw0ctmcpTZWNBhigK39O0sv0rFitYgRL/TxwZ3uMQTl6Ol3ixeRBMOHs6kC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwtFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QKsqUjq+8ahkVB7oiD8GNzEn9mHXltdwh79frB64uhBz35LYbISTOfFjfK3SYMkaSHJcUMhPWSxPAoCyYYUBAOUOP+lXs4bzqkASrRa9HwSgGP/jxzFKi3LwwKY00/4hEQbD3AE4GdwOsW3YrdXvO6cVTOu6zajIwi/eZP5R3Tf86JPIcx8gof6WRr9wfs/RxlMuFwPBlFmftYvlPzaM2+kLrmOV7PJgWPqxh2I7rwx9uDuiy8c2hoXXm44Yy0rI+Th6zYopPdG0VVB3bN2+HJZUqi2WLYt7T8I4T211vCs3xLsLsoOhcicQ0pQo3RvfZuSHc4eW5hLjU/6cITJii3JkfLKzng+y8VS8xuHlWMm4zVVHojZfntnDsXAN0BPT6syZRfdn4kih3jOP2xjS6uFCP080ibLWJ4A9zrM0jJYeskTOEjXolEnrjaKabFgo9+u05+j/Z7XpvJ6cN4t6igHkNaQun9SyAeA4MwgVUGmb+P6z2abs/U38WrpKj/k2nrPFv5DdIMQXvrS5DBNN0oY/9xa/CC+r38gfnXkeNV5KZBaHj5XyNFzVO/D5DfK/g0y2nztxxvDGOKfhApTXIXTZnrfhZ+U110kJ6wMpyZh0/ZtOG/lVK+j6QF7Zv8eeBRokdQG43rC0Js9609Y6WCeeC6jRAKLb+QuM9/k/IuCka4ocuTK7IP8gsa29xUQlkEMQKPH6laAcb2q1S7E/ex3AMCjcx+wZGGJPhTIQCenjiVmMSzlWPi/gUKc15zV9A4WjX96aGtKdxYeZ1SL+JaV4I3hcAwnVQ3jtfoSAHfwLbXDKe5Izonk/TbGkDrQZ+1SuuQv9keQ1K+PV/mgBqcqm2oElv6vckhY98TEyBMOYgTmA

Hello Karl,

The variable A must be made explicitly generalizable with

Generalizable Variable A.

Cheers,
Li-yao

On 03/30/2018 10:45 AM, Karl Crary wrote:

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