Re: [isabelle] _graph _grap_aux and _sumC



_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




On Wednesday, March 25, 2015 at 15:11:00 (+0100), Buday Gergely wrote:
 > 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
 > 
 > - Gergely

-- 




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