coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Laurent Thery <Laurent.Thery AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Hide I : True in match
Date: Fri, 27 Mar 2020 11:39:34 +0100
Autocrypt: addr=thery AT sophia.inria.fr; prefer-encrypt=mutual; keydata= mQENBE3a3V8BCADTeORKU7I7UmBBcs4VhSCq1IgKD8vdmdrGAlF3IJSFng7Fk8+MgS2gWYcS Ukf5t+rjNM3Z6brfYXc1naZlf2JPGHvAGiz8+TkXL+/ZA6+gAoIKy/iKyD+hCD8m92WH3rPH vCX6EJ44FEI7gUJ37GlTjvuP0I55vaFcwEg8nDgkALaCJvrSHtePuPKR1Q+9q2dgR7fTObal HYGMAsgT6k6n2ofe4Q6VFRLJhruU02qAfV5zgIoa3xgrTwSr4RRDILHttAw7EN6aLG6JycJ7 sPsPsiQzrd/tFsNbiHYeojJCkU2pDSQ3pBtXAJL/z2pMWTeTXvA60l9w0sDO7M3mkC3vABEB AAG0J0xhdXJlbnQgVGjDqXJ5IDxMYXVyZW50LlRoZXJ5QGlucmlhLmZyPokBOAQTAQIAIgUC TdrdXwIbAwYLCQgHAwIGFQgCCQoLBBYCAwECHgECF4AACgkQHHaWvRTi0tpIgggAnSUYcU2N uchXkGGwmPuLmvSUMiLkyFPs9GF2YF1ONOuJtpnQMcpsseCkcmIjESz0h5OpknpyraUXvbh0 ZdFqaLC2E+GyV8/YQi71wSsTPgWP450u0XUt0ysjwkKW6aIxIhSzrtgNp4E6w5KzXVJxA/yM V5RNFHg/5uifgfv4b7xaGHV8L93NbSvedk1O7yje5Hqgfab0t6J5Kf0M3sG+pB3gEkDVK9B7 +0fhe7/5u1Nj5HoLWid8UNZfFzJzb18Xe2ckzNye0KdDtQFac8qGUzhLbEYt3ScYjRYTq9/d V4Cin39j7Oo64Nk71iiLBISyuk0Q9D+Jq7nwwcQr/R8s1rkBDQRN2t1fAQgA7H6aX6BfdO/X Vlf4EGEoyFQ5u/JDe+giIHWSS34YWDWVUYyp320CrAYAkh9lQ1Nvh1tsmgiUh5xnY7wY0tOi wJSm94XlYAmHrddmWVNXRn09GvZJhfI2LdVBg3oxPfc8+bV+Hz83z/5BMPLOogxB22QMPJ6e iD2EsUMPNsuCVQ8WNo6ZmueuuYe7vEUXLYdRXNumJJgekEuG/q1BD4xgfzWpWfUODm6WygWZ oov50DomcDcAHW03bgnHlqnYu20Qg00GqgR3FKlORTvnOxD5TMCXe+eLUxkQfvnjbIPhtrnJ hgJMKVkRBEoaQ/XA4FdvxloInYPbqxNZ72yd09BbewARAQABiQEfBBgBAgAJBQJN2t1fAhsM AAoJEBx2lr0U4tLaWNQH/2/fIaF9ngbKPBJbDxYa7glJuCfamJgy3R8mJ//VYsS4RbdroSX3 29EgWlTx2reu1b4C5n5k7l4KpLgsRIc3bLUasGv15nf8BqmKIMulidzsxJv86S2imY/0870Q NOiO9SElHE7/2q4J1m2ew77SegiqGVWHl6Zs+4ROfOILTy24o26BQMAZhPX7jEs04Atv6yjw OUIPbzFO+XRuKqkBwHn9S8+GQelT0Gh84Dc5D2jIF0+kWY7uHqe2O+2LPfgO2CYhqmVfr/Ym mZv2xUyhJ7gui2hYaggncQ96cM2KhnKlgMw8nStY0GTqVXLEjPYblz8mqtF8aBPRSk/DjjrF QeI=

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