coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Samuel Gruetter <gruetter AT mit.edu>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Zify support for all instances of a type function
- Date: Fri, 14 Oct 2022 03:40:47 +0000
- Accept-language: en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gruetter AT mit.edu; spf=Pass smtp.mailfrom=gruetter AT mit.edu; spf=None smtp.helo=postmaster AT outgoing-exchange-3.mit.edu
- Ironport-data: A9a23:0/fzqKgz1LMVb7dyHCIW25YqX161rxQKZh0ujC45NGQN5FlHY01je htvDzjUaPvcMGrxKY1waIizpx8Bv5DVyt9jTlE+qi9nEShjpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UqicUsxIbVcMYD87jh5+kPIOjIdtgNyoayuAo tqaT/f3YTdJ4BYpdDNJg06/gEk35q6r4GpD5gdWic1j5TcyqVFFVPrzGonqdxMUcqEMdsamS uDKyq2O/2+x13/B3fv4+lpTWhRiro/6ZWBiuFIOM0SRqkQqShgJ70oOHKF0hXG7JNm+t4sZJ N1l7fRcQOqyV0HGsLx1vxJwS0mSMUDakVPKCSDXjCCd86HJW3r2+c9rHnosB6A32Pd+PE1D6 KQacQlYO3hvh8ruqF66Yu5xmsskLc/keY4PsXFpyz7USK1gRJHfBajG+Le03h9p1oYfW6yOI ZNCAdZsREyojxlnNU0KBY4ikf2Ag3jjNTBUtTp5oIJsuzaLnVEpjNABNvLVJ8KvY/RVsH3Fg WHlx3bVWUhFc+eAnG/tHnWE37KWxniTtJgpPLa/77thhECZ7ncCDQUfE1q9u/iwzECkM++zM GQT5zYhqqk0+wmmXtL9Vhu3rTvf+BsdR5xdH/BSBByxJrT84hyjPG0WdSR7RfMEpcYLaTE3j l3Qpoa8bdBwi4G9RXWY/7aSiDq9PykJMGMPDRM5oRs5D8rL/Nto0E6fJjp3OOvq14WkSW6YL yWi9XBm390uYdg3O7JXFLwtqxmlo5LTTwI66207tUr9tFoiNeZJi2G+gGU3AN5HMZqWSViHs z0Ji8Oe5eYBANTW0imMXKMAEKzBCxe53N/03wEH83oJrW7FF5ufkWZ4u24WyKBBaZlsRNMRS BWP0T69HbcKVJdQUYd5YpiqF+MhxrX6GNLuW5j8N4QQP8YhKV/crH0+OSZ8OlwBdmByzcnT3 r/FLK6R4YoyVMyLMRLsHr9Dj+V3rszA7TqIH8yTI+ubPUq2PSPMEuxt3Kqma+ki96qPoBjO/ spDLIOLzQ5DUfHjfiSf9oBbMV0BLX48AZf5uqRqmh2rfWJb9JUaI6aJm9sJItU994wMz7eg1 izjBidwlQSu7VWZcl/iQi44N9vSsWNX8ChT0doEZwj4ghDOoO+Hsc8iSnfAVeJ6rbI+nKMtF 6JtlgfpKq0ndwkrMg81NfHVxLGOvjzy7e5XF3r6MGoMbNR7ShbX+9TpWALq+WNcRmC0rMYy6 fnonA/SXZNJFUwoAdf0ecCf6Qq7nUEcv+ZuAGrOAN1YI3v3/KZQdifes/4QIuM3Eyvl+Ae07 QitLC0jlbH/mLNtqNjtroKYnritCNp7TxZ7HXGEzLOYNhv632uEwK1cWdaxYALibjrV+bqjV 8pR3frTIP0Kp3cUkoteQpJA77My2MvrnJBelj9bJXTsa0+6LI9gLl2t/9h9hocUypB34QKJC 1+yoP9EMrC3CebZOV82Jjt9SN+c1PsRywLg3d5sLGrUvCZIrae6C2NMNByxiQtYHrt/EKUh5 cwD4Mc2yQiOuiAGA+a8rBJ/1jqzdyQbcqAdqJslLpfhiVMrxnF8cJXsMHLKz6/VWepcEHsBA 2GytPLZiqV+13jyVSM5NULw0Np3gbUMvxF3z2E+GWmZp+qduNgJ2Ex+zDdmaCVU0RRN7MxrM EdJKUBeBPuD7hVotud5TkGuHABLOxnB3knPyFcytXb4SnOwXTfnN1wNOueq/WEY/VlDfzNdw qqq9Wb9XRvuf+DzxiEXW3M5m8f8TNd0yBLOqPqnE+uBAZM+Rzjv2Y2qWkYltDrlBpkXqHDch Ow34tt1V7L3BRQQr4I/FYOe87YaEzKABW5aRMBe7LE7Jn7ddB6yyAqxBRiIIO0VHMPz8Gi8F 8BKDeBMXU7n1C+x8xYqNZRVKLpwxPMU9N4Of43wHlE/spydkGtNkInR/S3AlmMUU41QscIiG LjwKROGMEKt3EVxpUGcjfN5KlKZYMYFbjLSxOqa0vsEPLNdvfBOcXMd6KqVvXKUOlBZpyDO7 RvJYqTK/dxiy41DsZbeSJhfIhTpNdrDbfm6zzrqktVRbOHgNdXFmBMVp2LGYSVXH+o1cPZmm YudtOXY2Bv+g483dGTCibytJrJs5/jubNFIM8nyEmZWrRGCVODo/REH3WKycr5Nr/9w+eilQ FGeRParVNtIRepY+mJZWxJeHzkZFa7zSKXq/gG5jvaUDykiwR71F8ym+VDpfFNkWHcxYbOmM TDNutGq+tx8h6ZPDkVdB/hZXrlJEGW6Uq4iL9DMpT2UC1ezuWy7u5zgq0sQ2WmeQD3MWsP3+ onMSRXCZQy/8vOAhs1Qt4tp+AYbFjBhiO03ZVgQ4MNylyv8NmMdMOABKt8TP/m4SMApOE3QP 1khrVfOCBkRmRxDbAnz59XlUUKSFucOM9H2K3lyuUaVd2G7CJ7o7H6NMMt/yy8eR9ch5LjPx RIiFrnYOxmthJxlWI7/I9Sl1Px/yKqyKm0goCjAfg+bP/raKbALyDpsEBcluekr1S3SvB2jG FXZjlyojK12pYAd3Cqgl7No9MklgQ7S
- Ironport-hdrordr: A9a23:OWJoOq8EtyyGwcEtevJuk+AUI+orL9Y04lQ7vn2ZESYlC/BxD6 iV7YUmPGzP+U4ssRYb6KC90ci7MA3hHPtOi7X5Uo3SOTUO1FHHEGgm1/qF/9SCIVyMygc+79 YFT0EWMrSZZjUX4voSojPIdOrIq+PmzEncv5a9854bd3AIV0gP1WZE402gYzZLrUF9dOAE/L H13Ls7m9K3EU5nEvhTKEN1INT+mw==
- Ironport-phdr: A9a23:Xsqy6RJ6+g3bXXayqNmcuE5vWUAX0o4c3iYr45Yqw4hDbr6kt8y7e hCFvrM23AaCAt+TwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnA JYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7ye6/94fdbghLmTaxbrF/I AurpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+V rxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4 aV2Rx/ykCoJNyA3/nzLisJ+j6xbrhCupx1jzIDbb46YL+Z+cbjHcN8GWWZNQsRcWipcCY28d YsPCO8BMP5FoYbnolsOsAWxBQ2xD+3u0D9Im2H53bEm0+s/CwHNwQstH90UsHTJstr1KLsSX v6vzKTTyDXDbu9W1S3j54fVbxAsuPeBVq9/fsTN00cgDR/FjkmOpoz/OTOYzucAvWaG4uduS e6iiHMqph1xrDahyMkiipfEi4IIx13Z+yt0wYY4KNO8RUNnYdCpE4dduSGHOodqTM0uXXxkt SI8x7Ybt5C7ey0Kx44mxx7Zc/GHfImI4g7jVOaMOjh0nm5qeLW6hxu07EOuyfX8W9Gp3FtJt CZIlsPAum4O2hDJ98SKRONx8lmu1DqV2Q3e5ftILV07mKbGMZIt37w9m5QLvUjeHSL6gkH7g LWZe0k+5+Sk9uvqb7P7rZGGLYB0kBvxMqE2l8y/H+s4Ng8OUnCc+eShyL3j8kr5QLRMjv05i 6XWrp/bKtgbpqGjBQ9V3Zgs5w+xAju81dQYnGUHIEhbdx2akojlI1DOIPbmAvejm1mgjTRmy +rCM7H7HJnALWLPnKrvcLpl7k5T0gszzdRR55JODbEBJer+WkDrtNzFEBA5LxC0zPj9CNhm0 4MeWH6PDrWHP6zPrF+E/uQvLPKUa48PpDn9M+Ql5+LpjXIhhFMRZbOp0ocPaHCkAvRmJF2Ub mbrgtcYCGsFog4+TPHxh1CZSj5SZ3OyX7om6T0hCYKmC53DRoG3j7Cb0ie7BM4eWmcTQFuLC DLjc5iOc/YKciObZMF72HRQXr+4DoQlyBuGtQngyrMhIPCCqQMCspe279Fw+uDX3T4o6DFoE 8mHmzWCVXx5gn8FXRcz3bw5rEBgnATQmZNkiuBVQIQAr8hCVR03YMa0J41SDtnzXlmEZdKVU BO9Rc3gBzgtT9U3yttIYkBnGtzkgAqQlzGyDeozkLqGTIcx7rqax2L4csln1nvayKQ7p1wnX o1COXD1zrVn+V3rDpXS216ci77scK0d2CDX82LWwnCTsV1EXRRYVKTZG30Texietsz3s2XFS bLmErE7Kk1BxMqFf7NNccHshE5aSe3LP8nCbGWwnWj1CAaDxrqKY4evICMY3TmbBUQZ++wK1 VCBMwV2RiKoomaFSSdrCUqqeET0t+93tHK8SEYwiQCMdUxokbSvqFYTgrSHRvUf06hh2m9po ihoHFu7w9PdCsaR7wtncqJGZNoh4VBBnWvHvg15N5akIuhsnFkbOwhwukrv0V1wBOAi2YAlt m4n0BZ/M4qd0U8Hej+FnNjxNrDRNmju7UW3caeFklra0duQ5uIO8KFh+xOy+lv5UBN5oBAFm 5FP3nCR54vHFl8XWJP1CQMs8gRi4qrdem877p/V0ntlNe+1tCXD0pQnHrhAqF7octFBPaeDD AK3HdcdAp3kJ/Y3lkS1YwgsOeFOsqM4Ion1EpnOkL7uJ+tmkD+82C5I+p1wzl6B7QJ5S/KO0 poYiaLQzk6MUDHyi02ku8b8lNVfZD0cKWG4zDDtGI9bYqAakZ8jMW61OIX3w9x/g8WoQHtE7 Bu4AEtA3sa1eB2UZli73AtK1E1Rr2b10Se/yjV1lXkuoM/9lGTB2fnvaAYKIEZORXUkgFvxa YS5lNEVWkG0YhNhzUvjtACgl+4C/+x2NCHLTF1NfjTqIm0qSaa2ureYIqstoNspvShRTOWgc AWfQ7/5rQEd1nCrFG9fyTYnMjCy78yp2U080jLbdS0gyRiRMdt9zhre+tHGEPtY3z5dATJ9l SGSHV+ked+g4dSTkZ7H9OG4TWOoEJNJIkyJhcuNsjW24WpyDFixhfe2z5foCxU3zTP2zfFvV DmOoRrhKNqOtezyIad8c09kCUWpocVgB4xijoYqrJQRxT4XiojfrjIX1Gz0N9tcw6f3anEAE CUKz9Di6w/gwER/L3iNytGcND3V0o57atK9eG9TxjMl4pUAFvKP9LId13g9sh+ioAnWe/Q4g joN1a5k9isBm+9Q8As1knfEUvZDWxAeZWu2y3Hqp5i/tPkFOTrpIej2jxs4zYnpDane8F8GH iyiPMd/W3YopsRnbACVgDusrNi6PoGXN4521FXckg+c3bEFbs13zKNM3W09ZSr8pSF3kr590 lo1gdfi+9LbY2R1oPDgUlgHcGOvIZtUoG2I7+4Wn97Kjdn/WMonRGVNBNyyEbqpCG5A7KSha EDRSXtk7S3HUbvHQV3GuAE36SiWVcjsbS3yRjFRzM0+FkDNYh0Z2l1SBHJgwtY4Dlz4nZynI QEjtnZJoQSk4hpUlrA2a1+mCDeZ+ljuM2lRKtDXLQIKvF8eoR6PYYrAsaQpR2lZ5sHz81bLd zHdPlgQSzFQEk2cWwK5Zufov4SGrLfeXLfbTbOGYK3S+7AGEabSg8rpisw/on6NLpndYyAkU 7tkgAwbGiolU8XBx2dSEmpK0X2XKZbc/kvZmGU/r9jjoqmyHl+ptdPJU/wIbp1u40zk3P7Fa 6jA3GAhbmwHnpIUmS2RlOJZhBhL1H4oLWXIc/xItDaRHvuMwOkPSUdLNGUuZINJ6ak4wwVAa /nA0oupjeYk16VtTV5YSVv6gs/vaMkDImX1cVrDAAzj2K2uAzrNzom3ZKq9TeYVl+BIr1irv i7dFUb/PzOFnj2vVha1MOgKgjvJdBpZ8JqwdBpgEw2BBJrvdwG7PdlrjDY33ax8h3XEMnQZO CR9dEUFp6OZ7CdRiPFyU2Jb6X8tIe6Bkiefp+7WT/Re+eNsGThxnvlG7W4SzKZJ4yZFQvMwl TvZrtdorFzjya+KyyYhXRZT635KiI+NoUR+KPDZ+51HChOmtFoG6WSdDQhPpsMwU42p6uYKm p6Wz/GWSn8K6d/f8MoCCtKBLcuGNCFkKh/1AHvPCxNDSze3NGbZjkgbkfeI93TToIJpz/qk0 JcIVLJfU0Q4U/0ADUEwVtMYPZprQj4+ubuakIgF6Wf0/3yzDI1K+4vKUP6fG6ClMDGCkbxNf AcF25v/MJgcMYz91AlvelJ6lYLFFg+LG9VMvmtsYhJ+8yAvuDBuC2Y03UzicAak5nQeQOW1k hABgQx7ee0x9T3o7j/fw3LPpTd2nUUsy42Nad+5dT/taqq8QNMPY8IVn08sLpz8QgB6KACil kxtMjjJAukXirp8M21nlV2E0aY=
- Ironport-sdr: 6348da44_SiCohgmvLqrrIp/VZIirtvdlDUFXx6loHILaVPmHFOYjYnF 6FnMEnOvW9nrguEfMJaYjyO8G86wDfmPKOkEo+Q==
I asked for parameterized zify instances a while ago, and the anwser
was that zify won't support them because of a strong restriction of the
implementation that is hardwired very deep:
https://github.com/coq/coq/issues/14054#issuecomment-812454419
But I think it should be possible to implement your own zify in Ltac
instead.
-----Original Message-----
From: Eddy Westbrook <westbrook AT galois.com>
Reply-To: coq-club AT inria.fr
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Zify support for all instances of a type function
Date: Thu, 13 Oct 2022 12:28:47 -0700
Hello Coq club,
I have a type function bitvector : nat -> Set that constructs the type
of bitvectors (binary numbers) of a given bit width. Is it possible to
get the zify tactic to support the class of types bitvector w for all
w? The existing Add Zify commands seem to only work for a specific
type.
Thanks,
-Eddy
- [Coq-Club] Zify support for all instances of a type function, Eddy Westbrook, 10/13/2022
- Re: [Coq-Club] Zify support for all instances of a type function, mukesh tiwari, 10/13/2022
- Re: [Coq-Club] Zify support for all instances of a type function, Pierre Vial, 10/13/2022
- Re: [Coq-Club] Zify support for all instances of a type function, Eddy Westbrook, 10/14/2022
- Re: [Coq-Club] Zify support for all instances of a type function, Kazuhiko Sakaguchi, 10/14/2022
- Re: [Coq-Club] Zify support for all instances of a type function, Chantal Keller, 10/14/2022
- Re: [Coq-Club] Zify support for all instances of a type function, Eddy Westbrook, 10/14/2022
- Re: [Coq-Club] Zify support for all instances of a type function, Pierre Vial, 10/13/2022
- Re: [Coq-Club] Zify support for all instances of a type function, Samuel Gruetter, 10/14/2022
- Re: [Coq-Club] Zify support for all instances of a type function, mukesh tiwari, 10/13/2022
Archive powered by MHonArc 2.6.19+.