[isabelle] does recdef function support distinct datatypes?

Dear users and developers,

Are functions where both sides of equality are not from the same datatype
supported by recdef functions?

If yes, how must be written the field "meansure"?

I did not find nothing looking like this in both sections from Isabelle
tutorial 3.5 (pg 47) and 9.2 (pg 178) talking about recdef.

I did not insert more datailed code becouse I don't think it is required. I
would show the code if it is necessary.

Thank you,
Lucas Cavalcante

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