Florian Sextl (Mar 12 2022 at 14:14): Florian Sextl (Mar 12 2022 at 14:14):Is there any way to rewrite top level term strings, e.g. in a similar way to how attributes can be used to rewrite theorems?
I'd like to have something like:
"(λx. snd x) (''a'',0)"[simplified] (*becomes the term "0"*)
"[1,0,1,0,0,1]"[drop_zero](*becomes the term "[1,1,1]"*)
These steps can be easily done with ML functions, but I don't know how to apply these to top level terms.
Background: I'm currently working on automation techniques based on Eisbach methods. Some of these methods take a user defined term string, which can for example be used as a pattern by a method that applies the frame rule of separation logic to all subterms that match the pattern. For this it would be quite handy (and for some ideas even necessary) to rewrite the term inputs in a specific way. I suspect the best way to do this would be with a custom parse_translation, yet I'd prefer a less "hacky" solution.
Last updated: Dec 21 2024 at 12:33 UTC