The Coq mailing list

[Math Prover <mathprover AT yahoo.com>]

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.

Attachment: test.v
Description: Binary data