coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: AUGER Cédric <Cedric.Auger AT lri.fr>
- Cc: "Coq Club" <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] inl and inr with both arguments inferred?
- Date: Mon, 26 Oct 2009 18:34:01 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
- Organization: ProVal
Le Mon, 26 Oct 2009 18:40:49 +0100, Brian E. Aydemir <baydemir AT cis.upenn.edu> a écrit:
Quoting Thorsten Altenkirch
<txa AT Cs.Nott.AC.UK>:
for my lecture I'd like to use sums (i.e. coproducts) so that both arguments of injections are inferred. Set Implicit Contextual doesn't seem to do the trick. Is there a way?
Set Contextual Implicit.
Definition ex2 : nat + bool := inl black.
If nothing else, you can use Implicit Arguments to explicitly declare the implicit arguments for a constant:
Implicit Arguments inl [A B].
Implicit Arguments inr [A B].
Definition ex2 : nat + bool := inl black. (* assuming black : nat *)
Hope that helps,
Brian
--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
You can also look "Set Implicit Arguments" and "Unset ..."
- [Coq-Club] inl and inr with both arguments inferred?, Thorsten Altenkirch
- Re: [Coq-Club] inl and inr with both arguments inferred?,
Brian E. Aydemir
- Re: [Coq-Club] inl and inr with both arguments inferred?, AUGER Cédric
- Re: [Coq-Club] inl and inr with both arguments inferred?, Matthieu Sozeau
- Re: [Coq-Club] inl and inr with both arguments inferred?,
Brian E. Aydemir
Archive powered by MhonArc 2.6.16.