The Coq mailing list

[Feró <ferenc.tamasi AT gmail.com>]

Speculations follow, I hope someone will correct me:

I guess, Check does not do "instantiation" only type checking, and for
that there's enough information.

If you do `Definition x := (assocList_r lst1 1).' instead of Check, it
will also fail. That is, Coq will not try to guess which decision
procedure you want to use as Keq.

On Sat, May 18, 2013 at 3:36 AM, Math Prover 
<mathprover AT yahoo.com>
 wrote:
> I'm using Coq 8.4 (downloaded from the main Coq website).
>
> In the following block of code (also attached), I get an "Error: Cannot
> infer the implicit parameter Keq of assocList_r." error.
>
> I believe what I have is a minimal example.
>
> What confuses me is that:
>
>   * when I use "Check" on the same types, it works
>
>   * when I define it as part of a Function, I get an "Cannot infer the
> implicit parameter" error
>
>
> Can someone please help me with:
>
>   1) Letting me know if there's anyway I can reformat my question to make it
> easier to answer. (Or any additional information I should provide.)
>
>   2) Tell me what I'm doing wrong / misunderstanding?
>
>
> ===== Code ======
>
>
> Require Import List Coq.Classes.EquivDec.
>
>
> Section assocList.
>
>   Variable K: Type.
>   Variable V: Type.
>
>   Variable Keq: forall k1 k2: K, {k1 = k2} + {k1 <> k2}.
>
>   Function assocList_r (lst: list (K * V)) (k: K) : option V :=
>     match lst with
>     | nil => None
>     | (k',v') :: xs =>
>       if Keq k k' then Some v' else assocList_r xs k
>     end.
>
> End assocList.
>
> Implicit Arguments assocList_r [K V Keq].
>
> Definition lst1 := (1,2)::nil.
>
> Check (assocList_r lst1 1).
>
> (* Up until this line, all works *)
>
>
> (* The following line gives me the error:
>   Error: Cannot infer the implicit parameter Keq of assocList_r.    *)
>
> Function f (lst: list (nat * nat)) (k: nat) :=
>   assocList_r lst k.



-- 
Give me liberty or give me cash!