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
- Re: [Coq-Club] implicitly generalizing binders: is this the expected behavior? (svn r13458), Tom Prince
- [Coq-Club] Re: implicitly generalizing binders: is this the expected behavior? (svn r13458), Adam Megacz
Archive powered by MhonArc 2.6.16.