The Coq mailing list

[Christopher Ernest Sally <christopherernestsally AT gmail.com>]

Well, I have to learn how to search my inbox better...

Thanks!

Best
Chris

On 19 June 2014 04:06, Jonathan <jonikelee AT gmail.com> wrote:

On 06/18/2014 04:03 PM, Christopher Ernest Sally wrote:

Hi all

I have a Section where I declare Variable foo : Type, and after I close the
Section, of course all my functions inside the section will have forall
foo: Type, etcetcetc.

My question is: Is there a neat way to get foo to be implicit? I only know
how to do it the usual way, but I have 30+ plus functions in the section...
and so wouldn't like a whole bunch of
Implicit Arguments fun1 [foo].
Implicit Arguments fun2 [foo].

Thanks

Warm regards
Chris

I asked the very same question a few weeks ago...

"Context {foo : Type}." does the trick.

-- Jonathan