coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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:
I asked the very same question a few weeks ago...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
"Context {foo : Type}." does the trick.
-- Jonathan
- [Coq-Club] Implicit Section Variables, Christopher Ernest Sally, 06/18/2014
- Re: [Coq-Club] Implicit Section Variables, Jonathan, 06/18/2014
- Re: [Coq-Club] Implicit Section Variables, Christopher Ernest Sally, 06/18/2014
- Re: [Coq-Club] Implicit Section Variables, Christopher Ernest Sally, 06/18/2014
- Re: [Coq-Club] Implicit Section Variables, Jonathan, 06/18/2014
- Re: [Coq-Club] Implicit Section Variables, Christopher Ernest Sally, 06/18/2014
- Re: [Coq-Club] Implicit Section Variables, Christopher Ernest Sally, 06/18/2014
- Re: [Coq-Club] Implicit Section Variables, Jonathan, 06/18/2014
Archive powered by MHonArc 2.6.18.