coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]

From: Jonas Oberhauser <s9joober AT gmail.com>
To: coq-club AT inria.fr, Math Prover <mathprover AT yahoo.com>
Subject: Re: [Coq-Club]
Date: Sat, 18 May 2013 11:45:15 +0200

Hi Math Prover,

Coq can not infer your decision procedure of type "forall K : Type, forall k1 k2: K, {k1 = k2} + {k1 <> k2}", which is an implicit parameter to this assocList_r function.

I believe the reason why "Check" works is similar to what Mr. Smolka was recently surprised to learn (and me too), namely that Check fills in evars with the gaps it cannot infer. Consider: https://sympa.inria.fr/sympa/arc/coq-club/2013-04/msg00058.html

Kind regards, Jonas

[Coq-Club], Math Prover, 05/18/2013
- Re: [Coq-Club], Jonas Oberhauser, 05/18/2013
- Re: [Coq-Club], Feró, 05/18/2013
  - Re: [Coq-Club], Math Prover, 05/18/2013
    - Re: [Coq-Club], Feró, 05/18/2013
      - Re: [Coq-Club], AUGER Cédric, 05/18/2013
      - Re: [Coq-Club] Infer Implicit Type of KEq, Math Prover, 05/18/2013