Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] inl and inr with both arguments inferred?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] inl and inr with both arguments inferred?


chronological Thread 
  • 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 ..."





Archive powered by MhonArc 2.6.16.

Top of Page