Lukas Stevens (Jul 16 2021 at 09:13): Lukas Stevens (Jul 16 2021 at 09:13):Was there ever any discussion on adding inner syntax antiquotations? What I am imagining here is that you can antiquote in Isabelle/HOL and just use some ML code to produce a term in the antiquoted place, e.g. definition "test = 1 + @{ML "HOLogic.mk_numeral 2"}. (The syntax is up for debate)
Manuel Eberl (Jul 16 2021 at 09:21):See here: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-June/msg00076.html
Manuel Eberl (Jul 16 2021 at 09:22):If you want to know more, ask Lars about it.
Last updated: Dec 21 2024 at 12:33 UTC