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
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