Re: [isabelle] \<^bsub> and \<^esub>

The Isabelle/Isar reference manual (available from the documentation panel) explains the general syntax of mixfix syntax annotations. They are normally enclosed in parenthesis and go between the type declaration and the "where" clause of fun/definition/inductive, etc. Alternatively, you can also use the command "notation" for functions that have already been defined. Examples of \<^bsub> \<^esub> can be found in library in theory Map.thy for the function restrict_map.


On 19/02/15 17:42, W. Douglas Maurer wrote:
\<^bsub> and \<^esub> cannot be part of the name of an identifier (variable, function,
constant, ...), they are meant to be used for subscripting terms in mixfix syntax. If
you want to have subscripts for identifiers, you must stick to \<^sub>. If the index
consists of several letters, each must carry its own \<^sub> as in x\<^sub>1\<^sub>2.
Conversely, when you define your own syntax for a function in which terms are
subscripted, only use \<^bsub> and \<^esub>, but not \<^sub>. Otherwise, you will get
strange effects.

Thank you for this. I have Krauss's "Defining Recursive Functions in Isabelle/HOL," which
is supposed to cover function definitions in general; however, searching this document
yields no instances of the word "subscript." Is there another document somewhere which
describes syntax definitions for functions in which terms are subscripted? Thanks! -WDMaurer
Prof. W. Douglas Maurer       Washington, DC 20052, USA
Department of Computer Science         Tel. (1-202)994-5921
The George Washington University Fax  (1-202)994-4875

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