Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Hide I : True in match


Chronological Thread 
  • From: Maximilian Wuttke <s8mawutt AT stud.uni-saarland.de>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Hide I : True in match
  • Date: Fri, 27 Mar 2020 11:14:14 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=s8mawutt AT stud.uni-saarland.de; spf=Pass smtp.mailfrom=s8mawutt AT stud.uni-saarland.de; spf=None smtp.helo=postmaster AT triton.rz.uni-saarland.de
  • Autocrypt: addr=s8mawutt AT stud.uni-saarland.de; keydata= mQINBFWVkZsBEADmp2Mq5XZcOg38F91SMR5uF8cqC7LaODrnF+xh3TNKgbK301sPwcSKA4gr +TKV73e4VQoWihiWaYfPJYHsudXrp644dqYvWuxNWlkh4S2HIOmcopuTEd063TL5hRvhkg0V ZOMq000ucKo0yBsUux7+TdZdDAX3WP1whF7jY8OTe5xnEO3yv4xydAZhbT/gMO/IW6BVE2xO eElXEwC8Tnssar8cM0wZcnxgKXq4dhjDO6sSkeaf81a6FPlpy+VuCIHFYoFIAquX6T6V+Zbi UXJyDSUSUVVmechLA8vXmiRgOTyVMdTejXQb5niLGjb/Upvy9uSlO7eR0aSkCs3vqeXIppmS PDTKVwPso/PmJHEJnZLrbXKqqh589pbDAdYfJvP3Sg0fncL5bzxV0gdSqWH0t0e7c9AMiHs5 5bxEHBXuVtNs1srF52gT0KlE84R2UOmZ9Kst7P3XgJtIGzuS5uSHqFmtknh9tj+/G/Kg3qDz njxM6xTGExNPHQuskwbvYDqA6/5Hslqis6D6EpMPGhRuUhPuE5Eb+PsxpV26UccZt51FqIIc Mwv+3AUPbF7v7s7rAE1BkbmClUGuYUGfqfndGT4V6fLpQH5F9kRdxmIm9FcMURUDvX4CBKZz gmwIZ4jgZ2jZ1VTy+MWIXRpgJIt5aim4liycyDoPk+fyYfdmQwARAQABtB1zOG1hd3V0dEBz dHVkLnVuaS1zYWFybGFuZC5kZYkCUAQTAQgAOwIbAQULCQgHAgYVCgkICwIEFgIDAQIeAQIX gBYhBD64TDV8welurJxMM+1Xu2bbvfzeBQJd7qlVAhkBAAoJEO1Xu2bbvfze9NkP92DvzDUh VM5IzQC+aK2M7Yo2NE5j3ELhZH1m+RZsU1Ek5evoBVX71WfIrBDHb92c5AUBPy3uzG9Rno2Y x6eE59BFr0CpGZ52G+JWjVxL2voBV8zuvI720lqHONv3zONK9OvaI0nE0XxV56NktzW6X018 8h4woo1amXu8jBxJcSdrwiS//T6ZqzrHAv00JWwmhbg57uwgvu07PcHDUSB93j8hx7RxP3UG bnTE1/3QRdwq4YDa/TO7v+EqEO8RCAlRtTCXnLlgRpIWPEx4+g4w9EGaBdc94YRgkEFh2U1z QuJt/3797P2iTiR3LqIXfSxTZUy/znMcy6q5Jl6A3+dms2JQRVjeA0yppajmxLDlz6zjZj91 BKIIXQbo5A8UiKDHWEgxq7Atyg/Bloc3njvaZ0+bGIKyciDT2Noyd8SHD4H390O/cD8LVjBt H6k/1wUFkX3h24dEFXASjA3vZCsmR/FI9wok9fyfpE/iqVXkUpmX20FNWJl9f9eLNSDKx7N7 foJSzwPVSGFSNhEY5BAjUkJrHOyHZ8tAShBJovxnIGfD2OtTqKLAEWHvm7+CYXeR91DjalPp /6iRd/xvRw6yisS+Nqi8X9gEBaq8vJemCV0psbU30brVs7dqKqaOf+N0PyCp/FDlCvYaAhEe kFgo4TeEqMe92xM49tzenY6I2vq5Ag0EVZWRmwEQALwwnvtVw/zFec+MNKgBwKt1MIG6EMBK c+OTIYM2tN4jcWlaAbEcIZGkBSeoPJeTi4m3GQXhifGZK29VoDIUQjYYDWNtp6U8y0hLRnqS VY/YvcTDnK929n5rqMqO0wYf1fzhmPshIyD1jj96tqu0ppX7zE++VQ/VJgVIA8IGcNXUN21A /+rJKCJFAvBp+6u2gNaUDfnqvPfTGtkq7A/D40Lo6y0KVu20R3W76iFWl6FEQzOe28VBnOjU /NbyzAzVUSgYCSfkYxhDiKfJRJvQd+VKUCAa+BSNoEPvDMKakvhApWUOncnNUbfXiH04fYSV iu2NH2Ls3HLm+6xaAaf9eUIU75A02xXUa6m+AccJQzCEJySeYJFVhJLSgZEbGwDZVdrRALol gYiIrwOHTitC2PLRej8HeywQrn3PUGBwiYdOa19KTHZykbO0s0SHb6bvm3vgpAPPdZp+QWPO Xx3aZz6dw4D867lisGVKMcKBcX9QCekVL7CW6lvvevUP5tBBYCshMvSTaN0BymBBwYrz8UB4 RYJ4cUs5apd1mMfD5Vm8EZf1DT15Q+K9+HsRQr3y/+AtHm0gd0DpXGfBH4H+54vyB9Aj3DVb yPMeFYv9UhyKALEomprFM0tr0+SPh275xXlIxUvoC+3PlFM0swoLSmi2Tu9edjU6GuyL91w/ 9WTjABEBAAGJBD4EGAEIAAkFglWVkZsCmwICKQkQ7Ve7Ztu9/N7BXaAEGQEIAAYFAlWVkZsA CgkQIA5mg0qOKkAoDhAAnms7o654V2uZWBsiiR2oEykGs/sIzxYcKrOi2RnkL6RAwhJgBr+W VpjQ2IS9IQ5Bxy8GOWhzyit2XvFYTWxGamrmyXol7IynGcl2U3WpmSQEPJx/QeyQ5lWLYzjn 5bbdzNdY0mhUnRZ+ke2tcttmvLsUKn2J/8lSyqBF4i4Yaj4p4LQ8n/K/eW9lIY+J/gVGDcrl ZqOozXV9aClYDtgxL/c6/TPuDi0vgkhIaojwsSu38YmhmbYP03ntiLTrLbjnJXr0pYIlMRqU mNvPsphOR8cVGFnZ50dVoWHSSJhoIESpu8Qz1qwvA9uNTDhe/nnr092diP78FWo4SENiKjrX A2fOjk0YoZA1uSL0RbcRKAttPC88iBWUyBwYrhMBFKzJeDG+lvBID8gED205Jy7Mk8v7R9Nq HpjJXST1avVMF7TXCH8OK7rgI9ATGLqJ31WoYZkCSFkYKYRbyarZnVKxMsQ1zhpjoEfuQlWa q2NgwS2cijWmKAmFV4Qv3FA5zAoEdzB9HCbT2DafITEUqjf111+WjNcfJvtfQcO7hghhMwFt W9Or9KqVKpEDrakuuHUr6nVnBNYCliY80m/X5DXOZsKzehxfHht4t+CydGE2xRzIwzpos2Ze bhkjWmghGS7G1JHADgEk7zBKyVxJm/nwwNGk5MdY9sckx8XMiaA5lV2oDw/+K7mXo2qbEPng hGjN2bAqYbZd/Wdh5SUwa5YvnfqWcSY7G8OA5pexnIV/5RRIdcc+RtrxADmfTYGVIvSfAS4u wALIgEd5LYdYBIajxWLCyNghoQowLqZbIQQ4eOWd2xCF6srcTsIou2kJ97iiFtXgX3PthKn+ fhdFYWktEDabDhgYSdqJVvs+Sk3lO41aJu5MSIsqWq+G0ZGumTtO/yR9x5RzA/qKn56S6Da8 WjRF6iq/oyemifyC74HXmmi6gd8HCWD+eEXNWVAVL/FlfYhL420olMcBgP+cMGJTpmWK5jCy axHH4RFYg8AAdzn0/Lc/Xr47IZBntCaLy3V1LSKvDSZackKOreBmxQrd2Qn5/seLYFWWl/rP vqib6hmoE17SjBI2szi/t37JGXTl0ZkhSUp6FSC4YmoFrKJgxuX0q7CONZzdZ9G7mNOkUdg3 QAaN6/EZQceGC/Dvi28jB57Y50OoOAcyJnSkS95lPobHcGbBDDIQVvcEBwhSir/coGXHk8tq MXCdhxDo9Tq1cSvANeRYuJdrTdJM2FMll7QEtBcto0DNCNEecvZ+D/uqOU+InyJHpD4qDpQR 8bqNJ3Fmehd54LYiZK2G5/gRwF+8vnaeoy9fSs/CAw3icKPTcSSmy9bOk3I0fgAyb63xLF/s GHAOq5gkPg+9o79dHcbtD425Ag0EVZWRmwEQAKYFa3Y6d5D34YkaNBYvjU3mUlaS2uq7khoV xhnPiad496PzpxpF76rwpAbh7+V+aqxFDldmydjV3REPgJKk5hnhJ2ndltaoy0CtzFOjUV2K kzzvG2YXADSKCqvLrtVx3wfAxOVxjPOlFzG57mvZd3MUlxOGJPvNbFJJY98OzjQGeCukITMO 4mivublSlJy8hNkwbMgkAfBkuITNXllrLfTxch6wikunYlDrtI2X1/h6ygXn/m8dYWzDGv80 PyzVHWNMz7JS5UuD7PkkazkqLzH9HQ+xj2x7KOWIHs9BQp99OrZfUMcD54EfoM0JUG5kq0Xs 099Z4UEFA2Pl+8mnn7z7NNZ1JSN0xjUuxhMu5deIkKEj8XGwB+6OXYEhF3mdh5T29C4LHDpp 3fpa9LU+8Dlpq0HJlwBx5ngXOfAmZrKAJhiy8kT3AfNskiVWxgYga2Kk2ku8vV4DkMai7kzK 45t0/cDwdgugeck83x/7yR9XIrBwlt8N4bdJ3URbOtnuGuYjM5RTtqpadjVLLr+ZdhKPdM7q tPfnHotjRq+ban1TdA/zlCOW+s4g955kvafY29qnhx54y+DQJUwELAZCTA0fT/eHs0n6M/gI LepMleBR7STA+XqnI5aWlWn3Pp6nI8t3bz0T6sFEocD++YJNEr/J7yduvcNaI84j03iRMfPj ABEBAAGJAh8EGAEIAAkFglWVkZsCmwwACgkQ7Ve7Ztu9/N4GJA//f21oF6/XClyTnbsNSBKL vbtb9CjKx+9c6B6k1qHePSylFf+BsrKFMEdtyn40bfVnQqQ1GzNFFbzGiFkUlwM1BZMR0ogl 6ahtJL3M4Tf7RkV6FUhkov5HwYIXDjx9WdboLPPz4NQkomgcWyc0vAndtL1vYFizVLkxIdWo nnv11M4MoQybCjv9lm+UwmoqLkSvrWn3F6RMPwsc4HWDRHiBYNkCxYGlfVfQax1u3ENH7KfE nZAEEoxSBkaha1Tv/06wHjQ9w+7ZwueiB48MCQleDM4xP+Geom/VIhExdySrAtGZEP7DjCpc XTYL6491G1gDdStpzSU0odKKxp3xUgB7gFuegBsM4dXm02Q6tzr+oVLkCeTGWld3/DfyIVVi 3f2w+g+JEE8W71GxuIw4IwuxXr0sGo1gHnH8CD5ky0/dGYfW644oZ6DQRzDqp+7sJNGoSOmE bJ5k7IgkPlwb41jNEz1miq/AIleDjVgM6ZP1g4eVAWgjATFqfv9y/WR1t1BvrcogGKdVLfRr 6kDYwP2GzzCGz2KiVtlPaPv52UYPa9zX6IT5hEOq4GSAVo2IHwtukyG10l7sanq7J6s5CumN ukDzuJxJ+EgNYIxaEtdujUPJxlRQcFwqjbLEt2LQBJivwzRhRmQfQz5tt3c797Tsto875TRg vFHu+ezStimb9ew=
  • Ironport-phdr: 9a23:6dW/dhDeJUPazCdwg83eUyQJP3N1i/DPJgcQr6AfoPdwSP75pMbcNUDSrc9gkEXOFd2Crakb26yL6+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6lX71zMZGw3+OAxpPay1X9eK14Xk+v6/4aLTYhlFwX+UKfM3dU3u7FaZis5Dqox7Yo011xGB9nBPYqFdwX5iDVOVhRf1oMmqqs1N6SNV7tco589FUKH7dqJwcqFEEDcrezQutMjiqgTfUSOU+mYQFHgQk19TCgHf6Bj8UtH9v32p5aJGxCCGMJiuHvgPUjO44vIuEkew0XZVB3sC6GjSz/dIoudeqROlqQZ4xtSOMpqJKfY4Y6XcOMgTTHBFV8BdESBMUNrlM9k/StEZNOMdlLHT4kMUpEHkVxKwGe+p1zlJw2T/1Lc+2uItVw3LjlR5QoA+9U/MpdCwD588FOC4yK6SkmffdfJK3jG78pqObxYg5OqFVKh0eMzdj0UiRVvI

Hi Club,

I would like to use the variable I in a pattern. Is it somehow possible
to hide the constructor `I : True` from the prelude, e.g. so that I need
to qualify it as `Coq.Init.Logic.I`?


> Fixpoint test (I : nat) : nat :=
> match I with
> | 0 => 0
> | S I => test I
> end.
> (* Toplevel input, characters 65-66: *)
> (* > Fixpoint test (I : nat) : nat := match I with | 0 => 0 | S I =>
> test I end. *)
> (* > ^ *)
> (* Error: Found a constructor of inductive type True while a constructor of
> nat is expected. *)


Thanks
Maximilian

Attachment: signature.asc
Description: OpenPGP digital signature




Archive powered by MHonArc 2.6.18.

Top of Page