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.
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…
The real question is why you would want that parsing of SML…
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 04:19 UTC