[isabelle] Looking up information about new datatypes
I am looking for an ML API for looking up information about new datatypes. In particular, from the name of
a datatype, I would like to find out the names (and types) of the selector functions corresponding to the
arguments of a constructor. I am aware of the get_info function from BNF_LFP_Compat, but this does not give
me any information about selector functions, since they were not supported by the old datatype package.
If I have understood the code correctly, get_info is based on the fp_sugar_of function from BNF_FP_Def_Sugar,
but this function mainly seems to return low-level internal information about the datatype. Is there a
function returning more high-level information, including the selector functions?
This archive was generated by a fusion of
Pipermail (Mailman edition) and