coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gregory Malecha <gmalecha AT eecs.harvard.edu>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Ltac unify expressions
- Date: Fri, 17 Feb 2012 16:44:18 -0500
- Authentication-results: mr.google.com; spf=pass (google.com: domain of gmalecha AT eecs.harvard.edu designates 10.60.18.163 as permitted sender) smtp.mail=gmalecha AT eecs.harvard.edu
Hello,
I am wondering if there is a better way to perform semantic equivalence checking in Ltac. Currently, I'm doing the following:
Ltac unifies a b :=
match a with
| b => true
| _ =>
let a := eval cbv in a in
let b := eval cbv in b in
match a with
| b => true
| _ => false
end
end.
It seems to work alright, but I would rather not fully evaluate the terms if I can help it, I'm going to end up running this a lot.
Thank you very much for any suggestions.
gregory malecha
- [Coq-Club] Ltac unify expressions, Gregory Malecha
- Re: [Coq-Club] Ltac unify expressions,
Adam Chlipala
- Re: [Coq-Club] Ltac unify expressions,
Gregory Malecha
- Re: [Coq-Club] Ltac unify expressions,
Adam Chlipala
- Re: [Coq-Club] Ltac unify expressions,
Matthieu Sozeau
- Re: [Coq-Club] Ltac unify expressions, Gregory Malecha
- Re: [Coq-Club] Ltac unify expressions,
Matthieu Sozeau
- Re: [Coq-Club] Ltac unify expressions,
Adam Chlipala
- Re: [Coq-Club] Ltac unify expressions,
Gregory Malecha
- Re: [Coq-Club] Ltac unify expressions,
Adam Chlipala
Archive powered by MhonArc 2.6.16.