The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

On Mon, Jul 22, 2013 at 1:03 AM, Matthieu Sozeau
<matthieu.sozeau AT gmail.com>
 wrote:
>
>> - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
>> Arguments elements _ _.
>> Print Implicit elements. (* Argument DM is implicit and maximally inserted 
>> *)
>> - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
>
> That's unfortunate, maybe a bug? You could try the [Implict Arguments 
> elements []]
> command instead.

On Mon, Jul 22, 2013 at 1:07 AM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:
>
> I think [Arguments elements : clear implicits.] might do what you want.

On Mon, Jul 22, 2013 at 1:10 AM, Robbert Krebbers
<mailinglists AT robbertkrebbers.nl>
 wrote:
>
> I do not think it is a bug. You should use
>
>   Arguments elements : clear implicits.

Indeed! Thanks!

>> Furthermore, it seems to break other things, like the `elements`
>> coercion I asked for with `:>`:
>>
>> - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
>> Goal forall x y: E, (In _ elements x) -> x ≺ y. (* works fine *)
>> Goal forall x y: E, (In _ dm x) -> x ≺ y. (* error *)
>> - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
>>
>> If I use a Record instead of a Class, the coercion works as expected,
>> but then the implicit argument inference for ≺ doesn't work. Can I
>> somehow have my cake and eat it too?
>
> :> in a Class declaration does not declare a coercion (as documented in the
> reference manual) but an instance. You can certainly make elements a 
> coercion
> afterwards using the [Coercion] command.

That doesn't seem to work either:

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Definition ESet := Ensemble E.

Class DM := {
  elements : ESet;
  order    : relation E
}.

Arguments elements : clear implicits.

Coercion elements: DM >-> ESet.

Parameter dm: DM.

Goal forall x, (In _ (elements dm) x). (* works fine *)
Goal forall x, (In _ dm x). (* error *)
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

Bug?

To ask an unrelated question: Why can't I use `Ensemble E` directly in
the Coercion declaration? Apparently it requires a single identifier.

Thanks,

--
www.mhelvens.net