The Coq mailing list

[Robbert Krebbers <mail AT robbertkrebbers.nl>]

The Context command should do this job.

For example:

Section sect.
  Context `{inst : type_class A}.

  Theorem thm : B ->  C.
  ...
End sect.

On 11/21/2011 09:38 PM, Michael Shulman wrote:
> Is it possible to declare a hypothesis in a section which will be
> automatically *implicitly* generalized upon completion of the section?
> In particular, I would like to do this for an instance declaration, so
> that
>
>    Section sect.
>
>      Hypothesis A : Type.
>      Hypothesis inst : type_class A.
>
>      Theorem thm : B ->  C.
>      ...
>
>    End sect.
>
> would be equivalent to
>
>    Theorem `{inst : type_class A} : B ->  C.
>
> I suppose that I can do this with
>
>    Implicit Arguments thm [[A] [inst]].
>
> (Is that literally the same thing, or is it going to miss out on some
> typeclass magic?)  In any case, that is tedious if the section
> contains many definitions and theorems.
>
> Mike