coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] test for term convertibility without instantiation
- Date: Sun, 30 Oct 2016 21:21:47 +0000
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f182.google.com
- Ironport-phdr: 9a23:iVqNCxJpjgWRkAcKjtmcpTZWNBhigK39O0sv0rFitYgULPnxwZ3uMQTl6Ol3ixeRBMOAuqgC1LWd6vy/EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuS9SU0Jv8jrzts7ToICxwzAKnZr1zKBjk5S7wjeIxxbVYF6Aq1xHSqWFJcekFjUlhJFaUggqurpzopM0r221qtvkg789NV7nhN+R9FOQATWduD2dgz8ry/TLHUAHHsnAbSyAdlgdCKwnD9hDzGJnr5HjUrO14jQuTJsrwBZ8uXi+5p/NpQQTvjigdMCUioUnYj8VxiORQpxf39E83+JLdfIzAbKk2RajaZ95PADMZBss=
You can assert the goal [term1 = term2], generalize over all of the evars, and then see if [reflexivity] solves your goal. Is this what you're looking for?
On Sun, Oct 30, 2016 at 4:38 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:
Is there any way in Ltac to test if two terms are convertible without
inducing any evar instantiation, and without doing unnecessary reduction?
-- Jonathan
- [Coq-Club] test for term convertibility without instantiation, Jonathan Leivent, 10/30/2016
- Re: [Coq-Club] test for term convertibility without instantiation, Jason Gross, 10/30/2016
- Re: [Coq-Club] test for term convertibility without instantiation, Jonathan Leivent, 10/30/2016
- Re: [Coq-Club] test for term convertibility without instantiation, Jonathan Leivent, 10/31/2016
- Re: [Coq-Club] test for term convertibility without instantiation, Jonathan Leivent, 10/30/2016
- Re: [Coq-Club] test for term convertibility without instantiation, Jason Gross, 10/30/2016
Archive powered by MHonArc 2.6.18.