The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Context allows you to do this:
<<<<
Class inhabited (A:Type):= {repr:A}.
Generalizable Variable A.
Section FOO.
  Context `{inhabited A}.
  Definition unsafe_head (l:list A) :=
    match l with
      | nil => repr
      | cons x _ => x
    end.
End FOO.
About unsafe_head.
(*
unsafe_head : forall A : Type, inhabited A -> list A -> A

Arguments A, H are implicit and maximally inserted
Argument scopes are [type_scope _ list_scope]
unsafe_head is transparent
Expands to: Constant Top.unsafe_head
*)
>>>

On Mon, Nov 21, 2011 at 9:38 PM, Michael Shulman 
<mshulman AT ucsd.edu>
 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
>