Email Gateway (Aug 22 2022 at 19:46): Email Gateway (Aug 22 2022 at 19:46):From: PAQUI LUCIO <paqui.lucio@ehu.es>
Hi all,
I'm learning to write methods using the Eisbach library. I have
problems with the matching mechanism for evaluating a term envolving
user-defined functions. I also have problems to do matching with a
term involving user-defined functions. For example, I cannot write a
Eisbach method with the same functionality of the following Ltac in
Coq (the code has been simplified to show only the relevant matters):
fun f:: 'a => 'a list := .....
Ltac apply_R :=
match goal with
| |- ( ... H ...) => let L := eval cbv in f(H)
in match L with
| nil => apply R
| _ => idtac
end
end.
Thanks in advance,
Paqui
Last updated: Nov 21 2024 at 12:39 UTC