coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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. :-)
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 => trueend|}.(* 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|}.
- [Coq-Club] Typeclass confusions, Benjamin C. Pierce, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Emilio Jesús Gallego Arias, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Gaetan Gilbert, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Benjamin Pierce, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Emilio Jesús Gallego Arias, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Gaetan Gilbert, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Emilio Jesús Gallego Arias, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Matthieu Sozeau, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Benjamin C. Pierce, 06/25/2017
- Re: [Coq-Club] Typeclass confusions, Matthieu Sozeau, 06/25/2017
- Re: [Coq-Club] Typeclass confusions, Matthieu Sozeau, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Emilio Jesús Gallego Arias, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Gaetan Gilbert, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Gaetan Gilbert, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Emilio Jesús Gallego Arias, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Abhishek Anand, 06/24/2017
Archive powered by MHonArc 2.6.18.