coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] Hide I : True in match, Maximilian Wuttke, 03/27/2020
- Re: [Coq-Club] Hide I : True in match, Laurent Thery, 03/27/2020
- Re: [Coq-Club] Hide I : True in match, Christian Doczkal, 03/30/2020
- Re: [Coq-Club] Hide I : True in match, Maximilian Wuttke, 03/31/2020
- Re: [Coq-Club] Hide I : True in match, Jason Gross, 03/31/2020
- Re: [Coq-Club] Hide I : True in match, Maximilian Wuttke, 03/31/2020
- Re: [Coq-Club] Hide I : True in match, Christian Doczkal, 03/30/2020
- Re: [Coq-Club] Hide I : True in match, Laurent Thery, 03/27/2020
Archive powered by MHonArc 2.6.18.