The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

Thank you!  Where can I find documentation about "Context"?  It is not
in the index of the Coq reference manual.  Nor is your "Generalizable
Variable" -- what does that do?

On Mon, Nov 21, 2011 at 13:32, Alexandre Pilkiewicz
<alexandre.pilkiewicz AT polytechnique.org>
 wrote:
> 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
>>
>