Brando Miranda (Dec 16 2021 at 16:53): Brando Miranda (Dec 16 2021 at 16:53):I was curious to know if there was a way to automatically convert Isabelle tactic script to Isar declarative scripts (I know there is no dichotomy but just to phrase the question). Mainly, because I was curious to see if the procedure would teach me anything to do something similar for Coq (to generate IsarCoq lol but that's besides the point, I am genuinly curious about how generate nice Isar like scripts in general and apply it somewhere later). Ideally, it would be nice with a little machine learning if possible. If it does require machine learning then perhaps ideally not deep learning at first (to do such conversions).
Reference: https://www.reddit.com/r/isabelle/comments/rh0mh7/is_there_an_automatic_way_to_generate_isar/ and https://stackoverflow.com/questions/70352908/is-there-an-automatic-way-to-generate-isar-scripts-given-a-correct-isabelle-tact
Last updated: Dec 03 2024 at 16:25 UTC