Email Gateway (Aug 18 2022 at 10:50): Email Gateway (Aug 18 2022 at 10:50):From: Lucas Cavalcante <thesupervisar@gmail.com>
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
Last updated: May 03 2024 at 12:27 UTC