Email Gateway (May 12 2021 at 03:00): Email Gateway (May 12 2021 at 03:00):From: Matthys Grobbelaar <m.grobbelaar@uq.net.au>
Hello,
I am currently creating a syntax translation which generates a set comprehension using data stored in the current theory context (a list of terms). However I am having issues generating the set comprehension structure.
For example, given the syntax \<lrel> x > x' \<rrel> with the list of terms [Free("x",...), Free("y", ...)] from the context, the resulting translation would be {((x, y), (x', y')). x > x'}.
At the moment, I've created a mapping for each term to its de Bruijn index in the comprehension and manually replaced all of the Free variables in the term provided by the syntax (i.e. x > x') with their Bound equivalents. However at this point I'm stuck since I have no idea how to then collect these terms into a final set comprehension with the appropriate structure and typing (a set of pairs of tuples where the tuple pairs depend on the context). I also feel like I may be overcomplicating things.
I've looked at the set comprehension parse_translation function in HOL/Set.thy however I'm not sure how it works to build the set itself. I noticed that it uses Syntax_Trans.mk_binder_tr which seems like something I may be able to use but I'm not certain about how it's supposed to be used.
Kind regards and thank you in advance,
Matthys Grobbelaar
Email Gateway (May 27 2021 at 12:58):From: Makarius <makarius@sketis.net>
Is this still open? Or did you somehow manage in the meantime?
(It usually helps to show the source text of concrete attempts.)
Makarius
Last updated: Jan 04 2025 at 20:18 UTC