Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Re: implicitly generalizing binders: is this the expected behavior? (svn r13458)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: implicitly generalizing binders: is this the expected behavior? (svn r13458)


chronological Thread 
  • From: Adam Megacz <megacz AT cs.berkeley.edu>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Re: implicitly generalizing binders: is this the expected behavior? (svn r13458)
  • Date: Fri, 05 Nov 2010 03:42:28 +0000
  • Cancel-lock: sha1:Ai7C0Msolg3zUfzo2Of78clPIbs=
  • Organization: Myself


Tom Prince 
<tom.prince AT ualberta.net>
 writes:
>>   (* even though [m] is reported as implicit, Coq still will not accept 
>> this: *)
>>   (*Context `(t2:class2 t).*)

> In `{} and `() binders, implicit arguments are ignored,

Hrm, I wasn't able to find any mention of this in the manual
(particularly not in section 2.7.17).  Is this an undocumented behavior?


> also works, (the ! turning off some of the magical properties of `().

I noticed the very brief mention of the bang (!) in section 18.5.1 a
while back, but wasn't able to figure out what it did.  It also doesn't
seem to be in the manual's BNF.


> As far as I can tell, the tricky bit is that the `{} and `() binders
> need to insert extra bindings before themselves, and so have to run
> when the syntax is being check, before Coq starts typechecking.  But
> coq only does the normal implicit argument checks and typclass
> resolution at typecheck time.

I see.

In retrospect, perhaps it would have been better to make implicit
generalization a property of *identifiers* being bound rather than
entire *binders*.  For example, instead of:

  Definition Param2 := True.
  Context `(MyClass Param1 Param2 Param3).
  (* Param1 and Param3 are generalized but Param2 is not *)

Putting the annotation mark directly on the identifier(s) the user wants
generalized:

  Context (MyClass `Param1 Param2 `Param3).
  (* Param1 and Param3 are generalized but Param2 is not *)

This leaves the case where a class has a huge number of implicit
arguments and the user wants all of them generalized -- in that case the
user would have to explicitly list them all and put the annotation mark
on each of them.  But perhaps that isn't a bad thing.

  - a




Archive powered by MhonArc 2.6.16.

Top of Page