[isabelle-dev] Exposing some functions of the API
jasmin.blanchette at inria.fr
Thu Oct 1 19:01:31 CEST 2015
Hi Florian, Frédéric,
Sorry for not answering this earlier. Somehow, I failed to notice that two of the three functions are my responsibility.
>> During some programming tasks, I had to use the following functions:
> note that these *_cmd functions are merely supposed to be used when
> declaring Isar commands; dervived Isabelle/ML code is always supposed to
> work with proper internalized entities (types term, typ, …). The
> corresponding interface is available as BNF_FP_Def_Sugar.co_datatypes.
This is sound advice. Nonetheless, I believe I read on this mailing list that it is good practice to export the "_cmd" functions. For the BNF package, we export many but not all of them. This is now rectified (484f7878ede4).
> Sounds reasonable at first sight. What do the maintainers of metis think?
Good idea (9f9b088d8824).
More information about the isabelle-dev