Email Gateway (Aug 19 2022 at 17:30): Email Gateway (Aug 19 2022 at 17:30):From: Buday Gergely <gbuday@karolyrobert.hu>
Hi,
having a function definition on datatypes, Isabelle creates some auxiliary definitions
_graph which takes the function's arguments uncurried and returns bool
_graph_aux ditto
_sumC which have the function's type but some types being uncurried
Where can I find a description of these? I have not found one neither in the Isabelle/Isar reference nor in the functions tutorial.
Cheers
Email Gateway (Aug 19 2022 at 17:30):From: Christian Urban <christian.urban@kcl.ac.uk>
_graph and _sumC are generated by the "standard" function
package and might be described there. However, the function
package usually hides cleverly these low-level definitions
such that you can go a long way without having to actually
understand what is going on (essentially behind the
pat_completeness and termination commands).
_graph_aux is a definition that is generated by the nominal
function variant, whose purpose is to make some function
definitions easier. How about we move the discussion about
tghis over to the nominal mailing list?
Christian
Email Gateway (Aug 19 2022 at 17:30):From: Christian Sternagel <c.sternagel@gmail.com>
If I remember correctly, Alexander Krauss' PhD thesis should give the
details of this internal constructions. -cheers chris
Last updated: Apr 25 2024 at 08:20 UTC