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.

	Florian


-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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