inl and inr with both arguments inferred?

[Thorsten Altenkirch]

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.

doesn't work.

Obviously, I'd prefer not to have to redefine the library functions...

Cheers,
Thorsten


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

--------------------------------------------------------
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

[AUGER Cédric]

Le Mon, 26 Oct 2009 18:40:49 +0100, Brian E. Aydemir  
<baydemir@...> a écrit:

> Quoting Thorsten Altenkirch <txa@...>:
>
>> 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 ..."

--------------------------------------------------------
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

[Brian E. Aydemir]

Quoting Thorsten Altenkirch <txa@...>:

> 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

[Matthieu Sozeau]

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

--------------------------------------------------------
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