Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Typeclass confusions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Typeclass confusions


Chronological Thread 
  • From: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Typeclass confusions
  • Date: Fri, 23 Jun 2017 19:08:56 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bcpierce AT cis.upenn.edu; spf=Pass smtp.mailfrom=bcpierce AT cis.upenn.edu; spf=None smtp.helo=postmaster AT hound.seas.upenn.edu
  • Ironport-phdr: 9a23:9qpTxhWHRGrvXKjT2+Giqx/KI6fV8LGtZVwlr6E/grcLSJyIuqrYYxGGt8tkgFKBZ4jH8fUM07OQ6PG/HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjSwbLdwIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/XlsN/g6xVrg+iqRJhxIDZe5uaOOZ7fq7HfdMWWWhMU8BMXCJBGIO8aI4PAvIPMetFsYb9oVkOogG7BQmtAuPk1yFFimXr1qMg0uQuDxvG0xA+EN4ArX/Zq876O7sKUeC00qbI1ynMYO1N1Djh6YjIaQotoeyUXb1ud8rRz1MjGB3YgVWNsIHoOS6e2OcVs2WD8uZtVeGih3Q6pwx/vjSj3MUhhpTTio4IxF3I6T11zYI0KNGiVkJ3f9ypHIFNuyyVM4Z6WMEvTmJutS0n0LMJo4S7czIPyJk/xx7QdfiHc4+Q7xLjU+aRPDF4i29/dLKkmRm961OgxvfhVsmszllKqCxFnsPSuX8Qyhzf8smHSv1j8Ue9wTuDygDe5+JeLUwpm6fXN4Qtz7wtmpYJrEjOEDP6lF3zjKCMd0Uk/uao6/7gYrXjvpKTLJN7ihn/MqswgMywHfo3PxMSUGia4uSwzqDj/VXnT7VMiP06iLfWv43HJcgDvK62HxdV0po/6xa4FzqpzNMYnWAeIF1ZfBKHkpPmNkrVIPH4CPe/m06jnC1qx/DAJL3hA4/CImLNkLf7Lv5B7BtXzxN2xtRC7bpVDKsAKbT9QBzfrtvdW1UTPgq2yuPmDp1WkMsmWG+VCaLTePfYukeJ6/gkLsGHZZRTpS7wLf5j6vLz2yxq0WQBdLWkiMNEIEuzGe5rdh2U

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
  |}.




Archive powered by MHonArc 2.6.18.

Top of Page