*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] How do I retrieve the mixfix syntax of a constant?*From*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Date*: Fri, 26 Mar 2010 20:41:17 +1100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <cc2478ab1003230729w79a7f9a4m8fd6824a1de894c5@mail.gmail.com>*References*: <4BA865C2.5070405@cse.unsw.edu.au> <cc2478ab1003230729w79a7f9a4m8fd6824a1de894c5@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.23 (X11/20090817)

Hi Brian, 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 (definedin Pure/Syntax/mixfix.ML). This function converts the mixfix into asyn_ext, which is a lower-level representation that is closer to whatactually gets stored in the theory data.

Evidently it is named "guess_infix" because it reconstructs ahigher-level "mixfix" value by looking at the low-level productionsstored in the theory's grammar. So it might not always succeed ifthere is anything unusual about the syntax for the given constant.

> [...]

According to the mercurial repository, this function was added byFlorian Haftmann in April 2008; maybe he could tell us more about itsexpected behavior.

Thanks for the advice! Sincerely, Rafal Kolanski.

**Follow-Ups**:

**References**:**[isabelle] How do I retrieve the mixfix syntax of a constant?***From:*Rafal Kolanski

**Re: [isabelle] How do I retrieve the mixfix syntax of a constant?***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Antiquotation for Theorem Names
- Next by Date: Re: [isabelle] Antiquotation for theorem names
- Previous by Thread: Re: [isabelle] How do I retrieve the mixfix syntax of a constant?
- Next by Thread: Re: [isabelle] How do I retrieve the mixfix syntax of a constant?
- Cl-isabelle-users March 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list