The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I've had trouble with instance/record notations in other contexts as well. 

Perhaps the tutorial should emphasize that one can always fall back to the basics and use the underlying constructor for the Inductive (typeclasses are just records, which are just Inductives):

(* fails with the same error: *)

Instance eqdecBool : EqDec bool := 

Build_EqDec _ _ Bool.eqb_prop.

(* succeeds: *)

Instance eqdecBool : EqDec bool := 

Build_EqDec bool _ Bool.eqb_prop.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Fri, Jun 23, 2017 at 7:08 PM, Benjamin C. Pierce <bcpierce AT cis.upenn.edu> wrote:

Many thanks for all the helpful responses to my query about typeclasses the other day.  I’m working on incorporating them into the tutorial I’m writing.  In the process, I’m generating fresh confusions. :-)

Can someone explain the following?  

Thanks!

   - Benjamin

Require Arith.

Require Bool.

Class Eq A :=

  {

    eqb: A -> A -> bool;

  }.

Instance eqBool : Eq bool :=

  {|

    eqb := fun (b c : bool) => 

       match b, c with

         | true, true => true

         | true, false => false

         | false, true => false

         | false, false => true

       end

  |}.

(* UNCOMMENTING THIS MAKES THE DECLARATION of eqdecBool FAIL (why??)...

Instance eqNat : Eq nat :=

  {|

    eqb := Arith.EqNat.beq_nat

  |}.

*)

Class EqDec (A : Type) {H : Eq A} := 

  { 

    eqb_leibniz : forall x y, eqb x y = true -> x = y 

  }.

(* ... BUT REMOVING THE |'s MAKES IT SUCCEED AGAIN (why??) *)

Instance eqdecBool : EqDec bool := 

  {|

    eqb_leibniz := Bool.eqb_prop

  |}.