Email Gateway (Nov 10 2022 at 10:51): Email Gateway (Nov 10 2022 at 10:51):From: Albert Jiang <albert594250@gmail.com>
Hello,
I wish to write an ML function that does the following: transform the name
of a fact to (Facts.ref * Token.src list) such that it can be used as part
of Sledgehammer_Fact.fact_override.
The requirement arises from the need to translate the command e.g.,
"sledgehammer (del: one_add_one)" in Isabelle/jEdit to Isabelle/ML. I only
have the name of the fact but not its proper representation for
Sledgehammer fact_override. I tried to look at what the parser does but
cannot decipher its behaviour. Therefore I would greatly appreciate a
succinct function that does the transformation specified above.
Many thanks,
Albert
Last updated: Apr 18 2024 at 16:19 UTC