Xiaokun Luan (Mar 13 2024 at 01:43): Xiaokun Luan (Mar 13 2024 at 01:43):Hi all,
I want to parse some Isabelle/ML files, is there any parser of Isabelle/ML? It seems that Isabelle/ML is a superset of Standard ML, and PolyML's parser cannot handle some features of Isabelle/ML.
Manuel Eberl (Mar 13 2024 at 10:53):This might be tricky due to the presence of antiquotations, which can run arbitrary ML code and depend on the Isabelle context in which they appear…
Mathias Fleury (Mar 13 2024 at 12:45):The real question is why you would want that parsing of SML…
Hanno Becker (May 02 2024 at 04:33):What exactly would you like to do? If it's about ML arguments (as in apply (tactic <{TACTIC>), where {TACTIC} is any ML expression of type tactic), one can do that
Last updated: May 04 2024 at 20:16 UTC