[isabelle] Eisbach methods



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.