coq-club AT inria.fr
Subject: The Coq mailing list
List archive
[Coq-Club] Tactic to check if a term is a "literal" (contains only constructors and names of inductive types)
Chronological Thread
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] Tactic to check if a term is a "literal" (contains only constructors and names of inductive types)
- Date: Mon, 14 May 2018 11:17:58 +0000
- Accept-language: de-DE, en-US
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga02.intel.com
- Dlp-product: dlpe-windows
- Dlp-reaction: no-action
- Dlp-version: 11.0.200.100
- Ironport-phdr: 9a23:ykeEUB8jrPQ/Sf9uRHKM819IXTAuvvDOBiVQ1KB31+wcTK2v8tzYMVDF4r011RmVBd6ds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55Pebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/2hikaKz43/mLZis1sg61Uux+uvQBzzorObY2JKPZyYKXQds4aS2pbWcZRUjRMDo2hYYsIEeUBMvpYr5P6p1sWtRe1GA6iBOLzxT9InHD5w6k63+o8GgzB2QwgHs4BsHTOo9rrMKceS/u1zK7WwjXMc/NWwzD96JDTfxAgp/GMQax/cc7LxUYzEAPFi0ydpIr4ND2b0eQNtnKU7+tmVe+3im4nrR1xrSarxss2l4bGmIQYwU3H+yVh2Is5ONO1RUFhbdK5HpZduDuWO5Z4T84jWW1kpjo2xqUbtZO6ciUG0poqyhDFZ/CZfYWF5gjvWPuSLDtlnH5pZbOyihKo/US+yuDxWdO43EhQoiZbndTBsnYA3AHJ5MedUPty5EKh1C6P1w/N7uFEJlg5la/UK5E73rI8iIAfsUXFHi/qhkr2iLWaeVkj+uit8+jnY7PmqYGAN4Jslw3zPKsjltaiDek2PQUCRXWX9Oq92bH540H1XK1GjvgsnanYtJDaK94bpqm8AwJN14Yj6gqwDze839sGmXkLNklFeBWZgIjmJ1HOOvf4De+kjlStljdr2+7JPrn7DprRKXjDla/tfaxh5E5E1Aoz0ddf6opIBbEGOfL/Q1P+tNjFDhAiKAG02ObmCNBl1owEQ26PA6mZMLnTsVCS/O4vLfOMN8cpv2O3IP88ovXqkHURmFkHfKDv04FdICSzGe0jKEGEa1LthM0AGCEEpFxtYvbtjQjIajleaGqoWLp4rhQ6A4KvAIOJDtSogbeB1Sq/WIZRa29aEFeUOXbua4iAHfwLbXTBcYdajjUYWO35GMca3ha0uVqikus1Hq/v4iQd8Knb+p1w7uzXmws18GUtXcWbz2yJCWpzmzFRHmNk7OVEuUV4j2y7/+1gmfUBTI5S4e9EVkExMpuOl7UnWeC3YRrIe5KycHjjQtiiBmhuHNc+yodUJUd7B9imyBvE2njyDg==
|
Dear Coq Team,
if I remember right, someone, I think it was Jason Gross, did implement a tactic to check if a term is “literal” (contains only constructors and names of inductive types) directly in OCaml. I have a version in Ltac, but it is complicated (requires things like a quod libet sandbox) and rather slow. But somehow I can’t find it in the manual nor in my emails nor in my older Coq projects nor in github. I guess I am just looking for a wrong name …
Best regards,
Michael Intel Deutschland GmbH |
- [Coq-Club] Tactic to check if a term is a "literal" (contains only constructors and names of inductive types), Soegtrop, Michael, 05/14/2018
Archive powered by MHonArc 2.6.18.