Re: [isabelle] Operator clash for $



On 16/06/16 12:08, Andreas Lochbihler wrote:
> Hi Manuel,
> 
> The $ notation is used also in other places of the HOL Library, e.g., in
> Library/FinFun_Syntax and HOLCF/Cfun. I'd recommend that the operations
> by default use subscripts for disambiguation, e.g. (we can discuss about
> the concrete subscripts),
> 
>   op $\<^sub>v for vectors
>   op $\<^sup>p for formal power series
>   op $\<^sup>f for FinFun

(This thread still seems to be unresolved.)

How about this?

  $ for vectors
  $\<^sup>p for formal power series
  $\<^sup>f for FinFun


> Then, if a user wants to use several of the theories at the same time,
> she can always use unambiguous syntax. However, typing subscripts can
> be annoying

How about this in etc/abbrevs?

"$" = "$\<^sub>f"
"$" = "$\<^sub>p"


	Makarius





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