coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] The implicit-argument-ness of type classes

From: Michiel Helvensteijn <mhelvens AT gmail.com>
To: Matthieu Sozeau <matthieu.sozeau AT gmail.com>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] The implicit-argument-ness of type classes
Date: Mon, 22 Jul 2013 10:08:12 +0200

On Mon, Jul 22, 2013 at 10:01 AM, Matthieu Sozeau
<matthieu.sozeau AT gmail.com>
wrote:
>
>> To ask an unrelated question: Why can't I use `Ensemble E` directly in
>> the Coercion declaration? Apparently it requires a single identifier.
>
> It's not unrelated, you can write Ensemble in the coercion declaration but
> not applied, the coercion just needs the head constant. Then [In _ dm x]
> checks.

Nice! Thanks!

--
www.mhelvens.net

[Coq-Club] The implicit-argument-ness of type classes, Michiel Helvensteijn, 07/22/2013
- Re: [Coq-Club] The implicit-argument-ness of type classes, Matthieu Sozeau, 07/22/2013
  - Re: [Coq-Club] The implicit-argument-ness of type classes, Jason Gross, 07/22/2013
  - Re: [Coq-Club] The implicit-argument-ness of type classes, Robbert Krebbers, 07/22/2013
  - Re: [Coq-Club] The implicit-argument-ness of type classes, Michiel Helvensteijn, 07/22/2013
    - Re: [Coq-Club] The implicit-argument-ness of type classes, Matthieu Sozeau, 07/22/2013
      - Re: [Coq-Club] The implicit-argument-ness of type classes, Michiel Helvensteijn, 07/22/2013