coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Matthieu Sozeau <mattam AT mattam.org>
To: Thorsten Altenkirch <txa AT cs.nott.ac.uk>
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 13:42:15 -0400
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi Thorsten,

Le 26 oct. 09 � 13:25, Thorsten Altenkirch a �crit :

Hi,

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.

You just need to redefine the implicits using:
<<
Implicit Arguments inl [ A B ].
Implicit Arguments inr [ A B ].
>>

Or you can [Import Program.Syntax] which will do this for you,
and declare maximal implicits for a few other standard datatypes.

-- Matthieu

[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