Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Implicit Section Variables

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Implicit Section Variables


Chronological Thread 
  • From: Christopher Ernest Sally <christopherernestsally AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Implicit Section Variables
  • Date: Thu, 19 Jun 2014 04:15:49 +0800

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





Archive powered by MHonArc 2.6.18.

Top of Page