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

Hi all,

> After more grepping, I did come across a function in
> Pure/Syntax/syntax.ML that looks like what you want:
> ML_val {* Syntax.guess_infix (Sign.syn_of @{theory}) @{const_syntax plus} *}
> val it = SOME (Infixl ("+", 65)) : Mixfix.mixfix option
> According to the mercurial repository, this function was added by
> Florian Haftmann in April 2008; maybe he could tell us more about its
> expected behavior.

This has been introduced by me to solve a technical issue concerning the
Haskabelle importer.  I would not recommend to use this.

> definition
>   "map_bp_any p ≡ λs. ∃v. map_bp p v s"
> (where map_bp was also defined using "definition") 

> In this case, I want to get out:
>     ("_ :→ _" [56,51] 56)
> so I can turn it into:
>     ("_ :→ -" [56] 56) 

Can you provide me with a little more context?  There are various ways
to deal with your problem, and the right way depends on how systematic
the desired behaviour can be described.




PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.