coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] test for term convertibility without instantiation

From: Jonathan Leivent <jonikelee AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] test for term convertibility without instantiation
Date: Sun, 30 Oct 2016 16:38:19 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f180.google.com
Ironport-phdr: 9a23:JVoyyRfufP3JqqqWmHLZc9mNlGMj4u6mDksu8pMizoh2WeGdxc66bB7h7PlgxGXEQZ/co6odzbGH6ea/BidZusvJ8ChbNscTB1ld0YRetjdjKfDGIHWzFOTtYS0+EZYKf35e1Fb/D3JoHt3jbUbZuHy44G1aMBz+MQ1oOra9QdaK3Iyfntq/8JzLYghOmCH1IfYrdE33/k3tsZw9hpIqAaIswFOdqXxRPu9S2GlAJFSJnh+66N3mr7B59CEFmfUn/tJAWKOyW6k5U7FeEHxyMWcz5c7msRTOZQSK73oYFG4Rl0wbUED+8BjmU8Kp4WPBve1n1XzfZJWuQA==

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