Re: [isabelle] How do I retrieve the mixfix syntax of a constant?
Brian Huffman wrote:
This is not as simple as it might seem, because mixfixes for
top-level constants are not actually stored anywhere. I did some
grepping of my own, and I found that when you declare a top-level
mixfix, it ultimately gets passed to Mixfix.syn_ext_consts (defined
in Pure/Syntax/mixfix.ML). This function converts the mixfix into a
syn_ext, which is a lower-level representation that is closer to what
actually gets stored in the theory data.
It is indeed not at all simple. I ended up just writing out the mixfix
representation by hand for the base constants, and they doing transforms
Purely out of interest, do you know how one can get the syn_ext for a
Evidently it is named "guess_infix" because it reconstructs a
higher-level "mixfix" value by looking at the low-level productions
stored in the theory's grammar. So it might not always succeed if
there is anything unusual about the syntax for the given constant.
According to the mercurial repository, this function was added by
Florian Haftmann in April 2008; maybe he could tell us more about its
As Florian indicated, that path doesn't look very stable. From examining
it, it seems the underlying syntax representation requires more time to
comprehend than I have.
Thanks for the advice!
This archive was generated by a fusion of
Pipermail (Mailman edition) and