The Coq mailing list

[Christian Doczkal <christian.doczkal AT inria.fr>]

Another possible trick is:

Definition I := I.

Fixpoint test (I : nat) : nat :=
  match I with
  | 0 => 0
  | S I => test I
  end.

This way, "I" can freely be used as a pattern variable while still being
convertible to "Logic.I"

Best,
Christian

On 3/27/20 11:39 AM, Laurent Thery wrote:
> 
> One possible trick is :
> 
> Fixpoint test (I : nat) : nat :=
>   match I with
>   | 0 => 0
>   | S (_ as I) => test I
>   end.
> 
> 
> On 3/27/20 11:14 AM, Maximilian Wuttke wrote:
>> Fixpoint test (I : nat) : nat :=
>>   match I with
>>   | 0 => 0
>>   | S I => test I
>>   end.