Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Hide I : True in match

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Hide I : True in match


Chronological Thread 
  • From: Christian Doczkal <christian.doczkal AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Hide I : True in match
  • Date: Mon, 30 Mar 2020 11:25:11 +0200

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.



Archive powered by MHonArc 2.6.18.

Top of Page