Hanno Becker (Sep 01 2023 at 06:26): Hanno Becker (Sep 01 2023 at 06:26):Hi. Can the toplevel interpret itself? I'd like to reduce boilerplate by introducing some macros, preparing sequences of toplevel commands as strings and interpreting them as if they had been written like that in the theory buffer. Is that possible?
So far, I always opened up the definition of the toplevel commands in question and replicated them in a piece of custom ML, but that is rather cumbersome.
Last updated: May 04 2024 at 08:17 UTC