Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] test for term convertibility without instantiation

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] test for term convertibility without instantiation


Chronological Thread 
  • 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





Archive powered by MHonArc 2.6.18.

Top of Page