coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Getting typeclass resolution to fail quickly?

From: "Paul A. Steckler" <steck AT stecksoft.com>
To: Jason Gross <jasongross9 AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>, Matthieu Sozeau <matthieu.sozeau AT inria.fr>
Subject: Re: [Coq-Club] Getting typeclass resolution to fail quickly?
Date: Wed, 1 Jun 2016 15:45:07 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=stecksoft AT gmail.com; spf=Pass smtp.mailfrom=stecksoft AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f65.google.com
Ironport-phdr: 9a23:ORTq4hXF2pJOgOFSbMKccmOwssrV8LGtZVwlr6E/grcLSJyIuqrYZhyEt8tkgFKBZ4jH8fUM07OQ6PCxHzFfqs/a6zgrS99laVwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oM2CJVgXz2PmOvtbF1afk0b4joEum4xsK6I8mFPig0BjXKBo/15uPk+ZhB3m5829r9ZJ+iVUvO89pYYbCf2pN4xxd7FTDSwnPmYp/4Wr8ECbFUrcrkcbB0cfiR1OSyff6wrhFsPzuzD9sOVn3zKBbOX5SLk1XXKp6KI9GzHyjyJSfQYw7WWfo4o4t75WqxGlqgY1i9rPfIyeN9JlYq7WfsgdS3YHVcFUAX8SSrigZpcCWrJSdd1TqJPw8h5X9UOz

On Wed, Jun 1, 2016 at 12:43 PM, Jason Gross
<jasongross9 AT gmail.com>
wrote:
> This means I need to be extremely careful to not put any lemmas in my
> rewriting databases which can utterly fail to be respected by any other
> relation (so any facts about [le] or [lt] are right out).

Maybe there are some heuristics to be applied here, since we can't
identify such lemmas in general.

-- Paul

Re: [Coq-Club] Getting typeclass resolution to fail quickly?, Abhishek Anand, 06/01/2016
- Re: [Coq-Club] Getting typeclass resolution to fail quickly?, Jason Gross, 06/01/2016
  - Re: [Coq-Club] Getting typeclass resolution to fail quickly?, Paul A. Steckler, 06/01/2016
    - Re: [Coq-Club] Getting typeclass resolution to fail quickly?, Matthieu Sozeau, 06/02/2016
      - Re: [Coq-Club] Getting typeclass resolution to fail quickly?, Jason Gross, 06/02/2016