Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Zify support for all instances of a type function

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Zify support for all instances of a type function


Chronological Thread 
  • From: Eddy Westbrook <westbrook AT galois.com>
  • 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
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=westbrook AT galois.com; spf=Pass smtp.mailfrom=westbrook AT galois.com; spf=None smtp.helo=postmaster AT mail-pf1-f182.google.com
  • Ironport-data: A9a23:6ZdeP6pFsJMgDTfeKGeI4TUJeZVeBmI4YRIvgKrLsJaIsI4StFCzt garIBmFb6mPMTenLoh3PIW+8xsCuZLRyNQ2TAJlrywyQytBpePIVI+TRqvSF3PLf5ebFCqLz O1HN4KedJhsJpP4jk3wWlQ0hSAkjclkfpKlVKiefHgZqTZMEE8JkQhkl/MynrlmiN24BxLlk d7pqqUzAnf8s9JPGj9Suv/rRC9H5qyo4mpA5wdmP5ingXeH/5UrJMJHTU2OByCgKmVkNrbSb /rOyri/4lTY838FYj9yuuuTnuUiG9Y+DCDW4pZkc/DKbitq+kTe5p0G2M80Mi+7vdkmc+dZk 72hvbToIesg0zaldO41C3G0GAkmVUFKFSOuzXWX6aSuI0P6n3TE2PhAM2opB6kk3dldL3NR9 vI8OSpdR0XW7w626OrTpuhEg80iKIzzMtpatCgwl3fWCvEpRZ2FSKLPjTNa9G1o14YeQLCEP pJfMGo1BPjDS0Un1lM/F58lgO2ygX78WzJRrFWUvuw85G27IAlZjuKxYYeJK4DiqcN9l1mCm z6X1jzDMzpCZNmTwBeqzyiIv7qa9c/8cNtKSOfQGuRRqFaU3ykYDAAcfUCqpOGwzE+4QdNWb UIOkhfCtoA3/U2vC8HzBli2+S7e+BEbXNVUHqsx7wTlJrfoDxixHWUqcRVeUvgak/Acay411 VGtjsm5LGk62FGKck61+rCRpDK0HCEaK24eeCMJJTfpBfGz/+nfaTqfEb5e/L6JYs7dQm6vn mjbxMQqr/BC0p5RjvTTEUXv2mr0/vD0ohgJChI7t19JAyt8bY+hIpSmsB3VtKYaaomeSVaFs T4PnM32AAEy4XOlxHPlrAYlRunBCxO53Nv03wcH834JqW3FxpJbVdoMiAyS3W8wWir+RRfnY VXIpSRa74JJMX2hYMdfOtzvVpp6kPi7Tou5Bpg4i+aihLAhJGdrGwk+NSatM5zFzSDAbIlla MjBKJn8ZZrkIfo7kmLeqxghPU8Dn3hinws/tLj0yBOo1bf2WZJmYeZtDbd6VchgtPnsiFyNr b53bpLWoz0CDrCWSnSIqeY7cwpWRVBlXsueg5IMJoa+zv9OQj5J5wn5muN/JeSIXs19yo/1w 51KchMBlwKu2yKZcFTih7IKQOqHYKuTZEkTZUQEVWtEEVB6CWp2xPdPLckEbvM8+fZ9zPV5a fAAdo/SSr5MUznLsXBVJ5X0sIUoJlzhiBOsLhiVRmE1X6dhYAjVpf7iXA/krxcVAgSN6MARn ryH1yHge6QleThMNsjtRciU/wuDhkRFwONWdGnUE+ZXY3TpodRLKTSur/oZIPMsCBTkxxmc5 jmGHx4ogPT8+d4p0djWhJKrq5WiPPt+E3F7QUjaz+eSHgvL8lWzxbRvVL6zQgncc2fv6YOeZ elx5NPtAs0txVplndJ1LOd28PgY+dDqmY5/8i1lO3f6N3KQFbJqJyi97/ll76Fi6OdQhlqrZ xip5NJfBLSuPfHlGn43IC4OTLyK9dMQqwnowcUFGmfIzw4pw+PfSmRXBQeGtwJFJrgsMI8F/ /YoiPRL1yOB0CgVIvS0pQEK0VTUNXERcbQVhrdDCq/Rtwcb4FVjY5vdNyzI3K+ye+h8akkEH hLEhY7ppaht+U7ZQn9iSVnPxbV8gLoNijBrzXgDBUi4pd7eos8d2ThqqDEScgtE6hBLzegpN nNZDBB3L//W/hNDpstKb0azES5vWTyb/U3QzQMStWv7FkOHaE3EHFcfC82son8L1n16fydK2 o2YxELOcyfYTOuo0gQcAUda+uHeF/pv/Qj8qeWbNsWiHahiRwH6g6WrNFE6mzG+Dewf3ET49 PRXpsBuYqjGNAkVka0xK6+e8Z8yEBmkBmhzcctNzZMzP1P3WW+NgGCVCkWLZMlyCeTA8ha4B +xQN8t/bUmC+xjUnA8LJ5wnAuFSrKYy6csga4HbAzcMk4GiowpDtLPS8SnDh1EXfeh+rPZlF KTvc2OtL2/Bo1pVhG7Hk+dcMEWaf9QvRVPxzcK1wsozBrMBt+BeK28p2OGwrVGQFhVtxDOPn Qb5f6SN5fdT+YdtuIrNE6t4GAS/L+3oZtmI6Ayet9dvb8vFFMXz6zMutVjsOjpJMYsrW9hYk aqHtPj11hjnuIkafn/4mZ7bMYV0/uS3AfRqN/zoIElgnSetXNHm5z0B8TuaLb1LiNZs2dm1d TCnacefdc8nZPkF/Sd7MxNhKhc6D7j7SozCpinn9vSFNUU74Dz9ddii8SfkUHFfeio2IKbBM w7Tucj/1uAA+c4ITFUBCup9CpB1HE77VOF0P5ftvD2fFS+zjknEprLmkgE65CrWDmWfVvz3+ o/BWgO0YSHaVHskFz2Fm9caUtwr4HdBbS0Ye0sc/5tuhWn/AjdWd6ISNpIJDpwSmSv3vH09i Pchc0N6YRgRnxwdGfk/3DgndgiWAusPIZHyITlBE4a8dXKtHI3ZaFd+3n4I3pq1EwcPCMmoI NUZ+2a2NR+0qn2sqSD/+dTj6dpaKjjmKr7kNKwzfwEew/rTPFnS6EFcIQ==
  • Ironport-hdrordr: A9a23:AQKATqHsPISP1z8EpLqE2ceALOsnbusQ8zAXPidKOHlom62j5q KTdZEgvyMc5wxhIU3I9erwW5VoP0msk6KdkLNhWYtKNTOO0ADJEGgL1+rfKlbbakrDH4BmpN 9dmmtFZOEYz2IWsS832maF+q4bsaK6GWmT69vj8w==
  • Ironport-phdr: A9a23:y+2vCBzHemvieNHXCzLRwFBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z heZvqU1xwaSAs3y0LFts6LuqafuWGgNs96qkUspV9hybSIDktgchAc6AcSIWgXRJf/uaDEmT owZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF5Ovn5FpTdgsip2e2+4ZPebgZUiDayfL9/I he7phjNu8cLhodvNrw/wQbTrHtSfORWy2JoJVaNkBv5+8y94p1t/TlOtvw478JPXrn0cKo+T bxDETQpKHs169HxtRnCVgSA+H0RWXgLnxVSAgjF6Bb6Xortsib/q+Fw1jWWMdHwQLspXzmp8 qVlRwLyiCofNzA27G7ZhcNtgqxYrhyvuRtxzpXIYIGMMfpyYqPdcc8ESWdHQ81fVzZBAoS5b 4YXAOQOIPtXrongrFQOsxS+HhWsC/j1yj9PgX/23rAx3uMvEA7YxwwgA8kBsG7TrNXyN6cfS u+1w7PMzTXEbvNWwi3x55TPchAkuPyBW697fsXNx0c1DQzFkkmQppL/PzOTzukAt2mW4uRjW OyghWAqpAJ8riayyssyhITEiYAYxkzY+Sh6xIs7JdO1RU50b9OnEZZdqS6XOpZrT80tTG9lp Tg3x7sbspC4ZCgH0IorywLbZvCdcIWF4gjvWPiMLTtknn5pZbGyiwiq/UWixODwTNe43VZQo iZYktTBtWoB2h3O5sWBV/Bz5F2u2SyV2ADW8uxEIV47la7cK5M5x74/jJsTsUDaEi/ulkX6k baadks59uWr9ejreLrmppibN497jgHxLL4ildC4AeQ9KgQOXm6b9vqg1LD740H1XLFHguc1n 6TZqpzWO9kXqrKjDwNI0Ysv9Q6zDzK839QZmXkHIkhFeBWCj4XxNVDBPuv4DeukjFS2lzdrw PPGM6buAprXKnjDl7bhfa1n50FAzwozyMhT55RPBb4ZOvL8RlfxtMDEDh8+KwG43v7rCM9h2 YMGRWKPHqiZPbvOvl+P/+IjOvWDZIsIuDnmMPUl/P7vjXohmVAHZ6Wp3J0XaGq5Hvt8OUmZb 2Ds0Z89FjIBuRN7R+j3ghXWWjlKIn22QqgU5zchCYvgA52VFa63h7nU8Su3D9Vpa3taAEqLF nSgI5qJQOsGciWVIedumzgDVKPnQIgkg0L9/DTmwqZqe7KHshYTsojugYAdD4z7kBgz8WYxF MGByySXSGoymGoURjgw1aQ5oEpny17F37Iry+dAG4l14PVEGhw/KYaa1/ZzXs//QR7LZNCOS 36pS9GhACp3RdU0kJcVe0goI9y5lVjY2jayRboclriFHpsxp73RxGT7PcF6yF7J3a0mjkJgS cxKZiW9nqAq0Q/VCsbSllmB0aancaNJxCnW6GKK1naDpmldWQ90FL3LBDURPxuM69v+4UzGQ vmlDrFP3hJp78mEJ+MKb9ToiQ8DX/L/IJHEZGn3nW6sBBGOz7fKbYzwemxb0j+PQE4D2xse+ 3qLL21cTm+ovn7eATpyFFnuf1Kk8O9wr2m+R1M1yAfCZlNo1r688BoYzfKGTPZb0rUBsSYn4 zJ6eTT1l83bEMaKvQ1mf41TaNc64UwB3mXc9kR8MpGmM6F+lwsGaQ0k90jq1hhxFsBBiZ1w9 CJsnFc0c/vAlgoRLWD9v9i4ILDcJ2js8Qr6bqfX3guby9OK4uIV7/9+rVz/vQavH05k8nN90 tAT3WHPg/eCRAcUT5/1VV46shZgoLSPKDYw/J/ez3prMoG7uzvF2slvD+wggEXFHZ8XIOafG Qn+HtdPTdejM/AggV+ubToLNeRV9bVyNMSjPajjuubjLKNrmzSoin5C6YZ23xeX9iZyfeXP2 o4M3/CS2gbvuy7UtF66qYi3nIlFYWtXBW+j0W3+A4UXYKRufIENAGPoIsutx9w4iYS/E3Jf8 VeiARsB1qrLMVKNYkfh1xdX0kc/rnWjniqjiTdzlnklo7Ge0yrH3+n5PEBfaygbGS841A+qe Njux9kBFFCldQ0oiAeo6SOYj+BAqaJzInOSCUZEci7qLn1zB665t76MeclKu9sjtSRaVvj5Y EjPEOas5UtHlXm6Ry0HlGpoElPi8o/0lBF7lm+HeXN6rX6DPNp12Q+a/tvXA/hYwjsBQiB8z zjRHFm1edezrrD239/OtP6zU2W5W9hday7umMmfuTCn73dtBh6XkPm3ndz8VwM91GWosrsiH TWNtxv6boTxgu6lPPl7dFNvA1zU5MN+HYBl1IA3gdtDvBpSzoXQ9n0Bn2DpNNxd0q+rd3sBS wkAxNvN6RTk0klufTqZgpj0XXKHzo59dsG3NykIjzkl4ZkAW8L2pPRU2DF4qV2ioUfNbOhhy 30DnOA25idSgvlV6lFwiHzMWvZIQRYeZWu2y1yJ94zs8vkRPj30N+HujAwm2onwadPK6gBEB CSnJNF7RXU2toMndwiUmHzrttO6Jp+KMYNV5kXSy1Ca16BUMM5jyaBM3HYhYDOn+yVikr5e7 1Qm3Inm7tfbbTw3oeThREYfb2O9ZttPqGi13eAHwZnQj8b3Wc84UjQTAMmxEqnuSWNO86yhb 0HXTlhe4j+aAeaNR1fOrhc76SuVQ9bzcCjIbHgBkYc4HUfbeRwZ2VFOGm19x89xFxj2lpa4L gEjvWFXvQS+8lwVm4cKf1HpW2Pb7m9Ecx8ST56SZFpT5wBGvQLONNCGq/h0FGde94GgqwqEL iqaYR5JBCcHQB7MAVerJbSo6dTalorQTuOjM/vDZ6mPou1CRr+Jw5yoyI5v4zeLMI2GIHBjC /Qx3kcLU2p+HozVnDAGSipfkCyoDYbTvBCn5ih+tdyy6tzuUQProJOBUv5caIU1vR+xhqiHO qibgyM4YTdU25UQxGPZnbgS2FlB7kMmPzKpELkGqWvMVPeKwv4RX0NdMXorcpIYtfFZvEEFI 8PQh9Lr26Qti/c0Dw0ATln9goSzYsdMJWihNVTBDULNNbKcJDSNzdukBMH0AbBWkuhQsAW9/ DiBFEq2dCuOjCXjTReoMslDhSWcPQcYs4a4OEUIayCrXJf9Zxu3PcUixyUx2qExj2jWOHQ0N DF9dwZVoOTV43oI2LNwHGtO6ncjJu6B0XX8jaGQOtMdtv1lBT5xnuRR7SEhyrdb2ypDQeR8h CrYqtMGS7SOneCLzTt8FhFJr2QT7GpklUprPaLY7d9LXnOWpXrlDE2VAhUO4sNrU5jh4vAKj NfIk633JXFJ9NeGpaMh
  • Ironport-sdr: 634866f3_8u76bVLFzGMtrGydq6JCvj9Z39okI5bW2GhWHZSio85AelM uyJOGvj5iPH6D2w+24bqXejMf/VgoTPJwaXkNMQ==

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


Archive powered by MHonArc 2.6.19+.

Top of Page