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"
This archive was generated by a fusion of
Pipermail (Mailman edition) and