chapter‹Inner syntax --- the term language \label{ch:inner-syntax}›
text‹
The inner syntax of Isabelle provides concrete notation for the main
entities of the logical framework, notably ‹λ›-terms with types and type
classes. Applications may either extend existing syntactic categories by
additional notation, or define new sub-languages that are linked to the
standard term language via some explicit markers. For example ▩‹FOO›~‹foo›
could embed the syntax corresponding for some user-defined nonterminal ‹foo›
--- within the bounds of the given lexical syntax of Isabelle/Pure.
The most basic way to specify concrete syntax for logical entities works via
mixfix annotations (\secref{sec:mixfix}), which may be usually given as part
of the original declaration or via explicit notation commands later on
(\secref{sec:notation}). This already covers many needs of concrete syntax
without having to understand the full complexity of inner syntax layers.
Further details of the syntax engine involves the classical distinction of
lexical language versus context-free grammar (see \secref{sec:pure-syntax}),
and various mechanisms for ∗‹syntax transformations› (see \secref{sec:syntax-transformations}). ›
🚫 @{command "typ"}~‹τ› reads and prints a type expression according to the
current context.
🚫 @{command "typ"}~‹τ :: s› uses type-inference to determine the most
general way to make ‹τ› conform to sort ‹s›. For concrete ‹τ› this checks if
the type belongs to that sort. Dummy type parameters ``‹_›'' (underscore)
are assigned to fresh type variables with most general sorts, according the
the principles of type-inference.
🚫 @{command "term"}~‹t› and @{command "prop"}~‹φ› read, type-check and
print terms or propositions according to the current theory or proof
context; the inferred type of ‹t› is output as well. Note that these
commands are also useful in inspecting the current environment of term
abbreviations.
🚫 @{command "thm"}~‹a1… an› retrieves theorems from the current theory
or proof context. Note that any attributes included in the theorem
specifications are applied to a temporary context derived from the current
theory or proof; the result is discarded, i.e.\ attributes involved in ‹a1, …, an› do not have any permanent effect.
🚫 @{command "prf"} displays the (compact) proof term of the current proof
state (if present), or of the given theorems. Note that this requires an
underlying logic image with proof terms enabled, e.g. ‹HOL-Proofs›.
🚫 @{command "full_prf"} is like @{command "prf"}, but displays the full
proof term, i.e.\ also displays information omitted in the compact proof
term, which is denoted by ``‹_›'' placeholders there.
🚫 @{command "print_state"} prints the current proof state (if present),
including current facts and goals.
The diagnostic commands above accept an optional list of ‹modes›, which is
appended to the current print mode; see also \secref{sec:print-modes}. Thus
the output behavior may be modified according particular print mode
features. For example, @{command "thm"}~▩‹("") symmetric› prints a theorem
without any special markup, bypassing the print mode setup of the Prover
IDE. ›
These configuration options control the detail of information that is
displayed for types, terms, theorems, goals etc. See also \secref{sec:config}.
🚫 @{attribute show_markup} controls direct inlining of markup into the
printed representation of formal entities --- notably type and sort
constraints. This enables Prover IDE users to retrieve that information via
tooltips or popups while hovering with the mouse over the output window, for
example. Consequently, this option is enabled by default for Isabelle/jEdit.
🚫 @{attribute show_consts_markup} controls printing of type constrains for
term constants; this requires @{attribute show_markup}.
🚫 @{attribute show_types} and @{attribute show_sorts} control printing of
type constraints for term variables, and sort constraints for type
variables. By default, neither of these are shown in output. If @{attribute
show_sorts} is enabled, types are always shown as well. In Isabelle/jEdit,
manual setting of these options is normally not required thanks to
@{attribute show_markup} above.
Note that displaying types and sorts may explain why a polymorphic inference
rule fails to resolve with some goal, or why a rewrite rule does not apply
as expected.
🚫 @{attribute show_consts} controls printing of types of constants when
displaying a goal state.
Note that the output can be enormous, because polymorphic constants often
occur at several different type instances.
🚫 @{attribute show_abbrevs} controls folding of constant abbreviations.
🚫 @{attribute names_long}, @{attribute names_short}, and @{attribute
names_unique} control the way of printing fully qualified internal names in
external form. See also \secref{sec:antiq} for the document antiquotation
options of the same names.
🚫 @{attribute eta_contract} controls ‹η›-contracted printing of terms.
The ‹η›-contraction law asserts prop‹(λx. f x) ≡ f›, provided ‹x› is not
free in ‹f›. It asserts ∗‹extensionality› of functions: prop‹f ≡ g› if prop‹f x ≡ g x› for all ‹x›. Higher-order unification frequently puts
terms into a fully ‹η›-expanded form. For example, if ‹F› has type ‹(τ → τ) → τ› then its expanded form is term‹λh. F (λx. h x)›.
Enabling @{attribute eta_contract} makes Isabelle perform ‹η›-contractions
before printing, so that term‹λh. F (λx. h x)› appears simply as ‹F›.
Note that the distinction between a term and its ‹η›-expanded form
occasionally matters. While higher-order resolution and rewriting operate
modulo ‹αβη›-conversion, some other tools might look at terms more
discretely.
🚫 @{attribute goals_limit} controls the maximum number of subgoals to be
printed.
🚫 @{attribute show_main_goal} controls whether the main result to be proven
should be displayed. This information might be relevant for schematic goals,
to inspect the current claim that has been synthesized so far.
🚫 @{attribute show_hyps} controls printing of implicit hypotheses of local
facts. Normally, only those hypotheses are displayed that are ∗‹not› covered
by the assumptions of the current context: this situation indicates a fault
in some tool being used.
By enabling @{attribute show_hyps}, output of ∗‹all› hypotheses can be
enforced, which is occasionally useful for diagnostic purposes.
🚫 @{attribute show_tags} controls printing of extra annotations within
theorems, such as internal position information, or the case names being
attached by the attribute @{attribute case_names}.
Note that the @{attribute tagged} and @{attribute untagged} attributes
provide low-level access to the collection of tags associated with a
theorem.
🚫 @{attribute show_question_marks} controls printing of question marks for
schematic variables, such as ‹?x›. Only the leading question mark is
affected, the remaining text is unchanged (including proper markup for
schematic variables that might be relevant for user interfaces). ›
The ∗‹print mode› facility allows to modify various operations for printing.
Commands like @{command typ}, @{command term}, @{command thm} (see \secref{sec:print-diag}) take additional print modes as optional argument.
The underlying ML operations are as follows.
🚫🚫‹print_mode_value ()› yields the list of currently active print
mode names. This should be understood as symbolic representation of
certain individual features for printing (with precedence from left to
right).
🚫🚫‹Print_Mode.with_modes›~‹modes f x› evaluates ‹f x› in an execution
context where the print mode is prepended by the given ‹modes›. This
provides a thread-safe way to augment print modes. It is also monotonic in
the set of mode names: it retains the default print mode that certain
user-interfaces might have installed for their proper functioning!
┉
The pretty printer for inner syntax maintains alternative mixfix productions
for any print mode name invented by the user, say in commands like @{command
notation} or @{command abbreviation}. Mode names can be arbitrary, but the
following ones have a specific meaning by convention:
▪▩‹""› (the empty string): default mode; implicitly active as last
element in the list of modes.
▪▩‹input›: dummy print mode that is never active; may be used to specify
notation that is only available for input.
▪▩‹internal› dummy print mode that is never active; used internally in
Isabelle/Pure.
▪▩‹ASCII›: prefer ASCII art over mathematical symbols.
▪▩‹latex›: additional mode that is active in {\LaTeX} document
preparation of Isabelle theory sources; allows to provide alternative
output notation. ›
section‹Mixfix annotations \label{sec:mixfix}›
text‹
Mixfix annotations specify concrete ∗‹inner syntax› of Isabelle types and
terms. Locally fixed parameters in toplevel theorem statements, locale and
class specifications also admit mixfix annotations in a fairly uniform
manner. A mixfix annotation describes the concrete syntax, the translation
to abstract syntax, and the pretty printing. Special case annotations
provide a simple means of specifying infix operators and binders.
Isabelle mixfix syntax is inspired by {\OBJ} cite‹OBJ›. It allows to
specify any context-free priority grammar, which is more general than the
fixity declarations of ML and Prolog.
The mixfix ‹template› may include literal text, spacing, blocks, and
arguments (denoted by ``‹_›''); the special symbol ``▩‹ı›'' (printed as
``‹ı›'') represents an index argument that specifies an implicit @{keyword
"structure"} reference (see also \secref{sec:locale}). Only locally fixed
variables may be declared as @{keyword "structure"}.
Infix and binder declarations provide common abbreviations for particular
mixfix declarations. So in practice, mixfix templates mostly degenerate to
literal text for concrete syntax, such as ``▩‹++›'' for an infix symbol. ›
subsection‹The general mixfix form›
text‹
In full generality, mixfix declarations work as follows. Suppose a constant ‹c :: τ1→… τn→ τ› is annotated by ‹(mixfix [p1, …, pn] p)›, where ‹mixfix› is a string ‹d0 _ d1 _ … _ dn› consisting of delimiters that
surround argument positions as indicated by underscores.
Altogether this determines a production for a context-free priority grammar,
where for each argument ‹i› the syntactic category is determined by ‹τi›
(with priority ‹pi›), and the result category is determined from ‹τ› (with
priority ‹p›). Priority specifications are optional, with default 0 for
arguments and 1000 for the result.🚫‹Omitting priorities is prone to
syntactic ambiguities unless the delimiter tokens determine fully bracketed
notation, as in ‹if _ then _ else _ fi›.›
Since ‹τ› may be again a function type, the constant type scheme may have
more argument positions than the mixfix pattern. Printing a nested
application ‹c t1… tm› for ‹m > n› works by attaching concrete notation
only to the innermost part, essentially by printing ‹(c t1… tn) … tm›
instead. If a term has fewer arguments than specified in the mixfix
template, the concrete syntax is ignored.
┉
A mixfix template may also contain additional directives for pretty
printing, notably spaces, blocks, and breaks. The general template format is
a sequence over any of the following entities.
🚫‹d› is a delimiter, namely a non-empty sequence delimiter items of the
following form: ▸ a control symbol followed by a cartouche ▸ a single symbol, excluding the following special characters: \\[\medskipamount] \begin{tabular}{ll} ▩‹'› & single quote \\ ▩‹_› & underscore \\ ‹ı› & index symbol \\ ▩‹(› & open parenthesis \\ ▩‹)› & close parenthesis \\ ▩‹/› & slash \\ ‹‹›› & cartouche delimiters \\ \end{tabular}
🚫▩‹'› escapes the special meaning of these meta-characters, producing a
literal version of the following character, unless that is a blank.
A single quote followed by a blank separates delimiters, without affecting
printing, but input tokens may have additional white space here.
🚫▩‹_› is an argument position, which stands for a certain syntactic
category in the underlying grammar.
🚫‹ı› is an indexed argument position; this is the place where implicit
structure arguments can be attached.
🚫‹s› is a non-empty sequence of spaces for printing. This and the following
specifications do not affect parsing at all.
🚫▩‹(›‹n› opens a pretty printing block. The optional natural number
specifies the block indentation, i.e. how much spaces to add when a line
break occurs within the block. The default indentation is 0.
🚫▩‹(›‹‹properties›› opens a pretty printing block, with properties
specified within the given text cartouche. The syntax and semantics of
the category @{syntax_ref mixfix_properties} is described below.
🚫▩‹)› closes a pretty printing block.
🚫▩‹//› forces a line break.
🚫▩‹/›‹s› allows a line break. Here ‹s› stands for the string of spaces
(zero or more) right after the slash. These spaces are printed if the break
is ∗‹not› taken.
┉
Block properties allow more control over the details of pretty-printed
output. The concrete syntax is defined as follows.
Each @{syntax entry} is a name--value pair, but the latter is optional. If
the value is omitted, the default depends on its type (Boolean: ▩‹true›,
number: ▩‹1›, otherwise the empty string). The following standard block
properties are supported:
▪‹indent› (natural number): the block indentation --- the same as for the
simple syntax without block properties.
▪‹open_block› (Boolean): this block has no impact on formatting, but it
may carry markup information.
▪‹consistent› (Boolean): this block has consistent breaks (if one break
is taken, all breaks are taken).
▪‹unbreakable› (Boolean): all possible breaks of the block are disabled
(turned into spaces).
▪‹markup› (string): the optional name of the markup node. If this is
provided, all remaining properties are turned into its XML attributes.
This allows to specify free-form PIDE markup, e.g.\ for specialized
output.
▪‹notation› (cartouche): a semi-formal description of the notation that
is surrounded by the block parentheses. The cartouche consists of multiple
words (separated by white-space). The first word specifies the ∗‹kind› of
notation as follows:
▪ @{notation_kind_def mixfix}: general mixfix notation, with delimiters
surrounding its arguments.
▪ @{notation_kind_def prefix}: notation with delimiter before its
argument.
▪ @{notation_kind_def postfix}: notation with delimiter after its
argument.
▪ @{notation_kind_def "infix"}: notation with delimiter between its
arguments (automatically inserted for @{keyword "infix"} annotations,
see \secref{sec:infixes}).
▪ @{notation_kind_def "binder"}: notation that binds variables within
its body argument (automatically inserted for @{keyword "binder"}
annotations, see \secref{sec:binders}).
▪ @{notation_kind_def literal}: notation for literal values, such as
string or number.
▪ @{notation_kind_def type_application}: application of a type
constructor to its arguments.
The mixfix template ▩‹"(_›~‹sy›▩‹/ _)"› specifies two argument positions;
the delimiter is preceded by a space and followed by a space or line break;
the entire phrase is a pretty printing block.
The alternative notation ▩‹(›‹sy›▩‹)› is introduced in addition. Thus any
infix operator may be written in prefix form (as in Haskell), independently
of the number of arguments. ›
subsection‹Binders \label{sec:binders}›
text‹
A ∗‹binder› is a variable-binding construct such as a quantifier. The idea
to formalize ‹∀x. b› as ‹All (λx. b)› for ‹All :: ('a → bool) → bool›
already goes back to cite‹church40›. Isabelle declarations of certain
higher-order operators may be annotated with @{keyword_def "binder"}
annotations as follows:
This introduces concrete binder syntax ‹sy x. b›, where ‹x› is a bound
variable of type ‹τ1›, the body ‹b› has type ‹τ2› and the whole term has
type ‹τ3›. The optional integer ‹p› specifies the syntactic priority of the
body; the default is ‹q›, which is also the priority of the whole construct.
Internally, the binder syntax is expanded to something like this: \begin{center} ‹c_binder ::›~▩‹"›‹idts → τ2→ τ3›▩‹" ("(3›‹sy›▩‹_./ _)" [0,›~‹p›▩‹]›~‹q›▩‹)› \end{center}
Here @{syntax (inner) idts} is the nonterminal symbol for a list of
identifiers with optional type constraints (see also \secref{sec:pure-grammar}). The mixfix template ▩‹"(3›‹sy›▩‹_./ _)"› defines
argument positions for the bound identifiers and the body, separated by a
dot with optional line break; the entire phrase is a pretty printing block
of indentation level 3. Note that there is no extra space after ‹sy›, so it
needs to be included user specification if the binder syntax ends with a
token that may be continued by an identifier token at the start of @{syntax
(inner) idts}.
Furthermore, a syntax translation to transforms ‹c_binder x1… xn b› into
iterated application ‹c (λx1. … c (λxn. b)…)›. This works in both
directions, for parsing and printing. ›
Commands that introduce new logical entities (terms or types) usually allow
to provide mixfix annotations on the spot, which is convenient for default
notation. Nonetheless, the syntax may be modified later on by declarations
for explicit notation. This allows to add or delete mixfix annotations for
of existing logical entities within the current context.
🚫 @{command "type_notation"}~‹c (mx)› associates mixfix syntax with an
existing type constructor. The arity of the constructor is retrieved from
the context.
🚫 @{command "no_type_notation"} is similar to @{command "type_notation"},
but removes the specified syntax annotation from the present context.
🚫 @{command "notation"}~‹c (mx)› associates mixfix syntax with an existing
constant or fixed variable. The type declaration of the given entity is
retrieved from the context.
🚫 @{command "no_notation"} is similar to @{command "notation"}, but removes
the specified syntax annotation from the present context.
🚫 @{command "write"} is similar to @{command "notation"}, but works within
an Isar proof body. ›
section‹The Pure syntax \label{sec:pure-syntax}›
subsection‹Lexical matters \label{sec:inner-lex}›
text‹
The inner lexical syntax vaguely resembles the outer one
(\secref{sec:outer-lex}), but some details are different. There are two main
categories of inner syntax tokens:
▸∗‹delimiters› --- the literal tokens occurring in productions of the given
priority grammar (cf.\ \secref{sec:priority-grammar});
▸∗‹named tokens› --- various categories of identifiers etc.
Delimiters override named tokens and may thus render certain identifiers
inaccessible. Sometimes the logical context admits alternative ways to refer
to the same entity, potentially via qualified names.
┉
The categories for named tokens are defined once and for all as follows,
reusing some categories of the outer token syntax (\secref{sec:outer-lex}).
The token categories @{syntax (inner) num_token}, @{syntax (inner)
float_token}, @{syntax (inner) str_token}, @{syntax (inner) string_token},
and @{syntax (inner) cartouche} are not used in Pure. Object-logics may
implement numerals and string literals by adding appropriate syntax
declarations, together with some translation functions (e.g.\ see 🚫‹~~/src/HOL/Tools/string_syntax.ML›).
The derived categories @{syntax_def (inner) num_const}, and @{syntax_def
(inner) float_const}, provide robust access to the respective tokens: the
syntax tree holds a syntactic constant instead of a free variable.
Formal document comments (\secref{sec:comments}) may be also used within the
inner syntax. ›
text‹
A context-free grammar consists of a set of ∗‹terminal symbols›, a set of ∗‹nonterminal symbols› and a set of ∗‹productions›. Productions have the
form ‹A = γ›, where ‹A› is a nonterminal and ‹γ› is a string of terminals
and nonterminals. One designated nonterminal is called the ∗‹root symbol›.
The language defined by the grammar consists of all strings of terminals
that can be derived from the root symbol by applying productions as rewrite
rules.
The standard Isabelle parser for inner syntax uses a ∗‹priority grammar›.
Each nonterminal is decorated by an integer priority: ‹A(p)›. In a
derivation, ‹A(p)› may be rewritten using a production ‹A(q) = γ› only
if ‹p ≤ q›. Any priority grammar can be translated into a normal
context-free grammar by introducing new nonterminals and productions.
┉
Formally, a set of context free productions ‹G› induces a derivation
relation ‹⟶G› as follows. Let ‹α› and ‹β› denote strings of terminal or
nonterminal symbols. Then ‹α A(p) β ⟶G α γ β› holds if and only if ‹G›
contains some production ‹A(q) = γ› for ‹p ≤ q›.
┉
The following grammar for arithmetic expressions demonstrates how binding
power and associativity of operators can be enforced by priorities.
\begin{center} \begin{tabular}{rclr} ‹A(1000)› & ‹=› & ▩‹(›‹A(0)›▩‹)›\\ ‹A(1000)› & ‹=› & ▩‹0›\\ ‹A(0)› & ‹=› & ‹A(0)›▩‹+›‹A(1)›\\ ‹A(2)› & ‹=› & ‹A(3)›▩‹*›‹A(2)›\\ ‹A(3)› & ‹=› & ▩‹-›‹A(3)›\\ \end{tabular} \end{center}
The choice of priorities determines that ▩‹-› binds tighter than ▩‹*›, which
binds tighter than ▩‹+›. Furthermore ▩‹+› associates to the left and ▩‹*› to
the right.
┉
For clarity, grammars obey these conventions:
▪ All priorities must lie between 0 and 1000.
▪ Priority 0 on the right-hand side and priority 1000 on the left-hand
side may be omitted.
▪ The production ‹A(p) = α› is written as ‹A = α (p)›, i.e.\ the
priority of the left-hand side actually appears in a column on the far
right.
▪ Alternatives are separated by ‹|›.
▪ Repetition is indicated by dots ‹(…)› in an informal but obvious way.
Using these conventions, the example grammar specification above
takes the form: \begin{center} \begin{tabular}{rclc} ‹A› & ‹=› & ▩‹(›‹A›▩‹)›\\
& ‹|› & ▩‹0› & \qquad\qquad\\
& ‹|› & ‹A›▩‹+›‹A(1)› & ='color:green'>‹(0)›\\
& ‹|› & ‹A(3)›▩‹*›‹A(2)› & yle='color:green'>‹(2)›\\
& ‹|› & ▩‹-›‹A(3)› & e='color:green'>‹(3)›\\ \end{tabular} \end{center} ›
subsection‹The Pure grammar \label{sec:pure-grammar}›
text‹
The priority grammar of the ‹Pure› theory is defined approximately like
this:
┉
Here literal terminals are printed ▩‹verbatim›; see also \secref{sec:inner-lex} for further token categories of the inner syntax. The
meaning of the nonterminals defined by the above grammar is as follows:
🚫 @{syntax_ref (inner) any} denotes any term.
🚫 @{syntax_ref (inner) prop} denotes meta-level propositions, which are
terms of type typ‹prop›. The syntax of such formulae of the meta-logic is
carefully distinguished from usual conventions for object-logics. In
particular, plain ‹λ›-term notation is ∗‹not› recognized as @{syntax (inner)
prop}.
🚫 @{syntax_ref (inner) aprop} denotes atomic propositions, which are
embedded into regular @{syntax (inner) prop} by means of an explicit ▩‹PROP›
token.
Terms of type typ‹prop› with non-constant head, e.g.\ a plain variable,
are printed in this form. Constants that yield type typ‹prop› are expected
to provide their own concrete syntax; otherwise the printed version will
appear like @{syntax (inner) logic} and cannot be parsed again as @{syntax
(inner) prop}.
🚫 @{syntax_ref (inner) logic} denotes arbitrary terms of a logical type,
excluding type typ‹prop›. This is the main syntactic category of
object-logic entities, covering plain ‹λ›-term notation (variables,
abstraction, application), plus anything defined by the user.
When specifying notation for logical entities, all logical types (excluding typ‹prop›) are ∗‹collapsed› to this single category of @{syntax (inner)
logic}.
🚫 @{syntax_ref (inner) index} denotes an optional index term for indexed
syntax. If omitted, it refers to the first @{keyword_ref "structure"}
variable in the context. The special dummy ``‹ı›'' serves as pattern
variable in mixfix annotations that introduce indexed notation.
🚫 @{syntax_ref (inner) idt} denotes identifiers, possibly constrained by
types.
🚫 @{syntax_ref (inner) idts} denotes a sequence of @{syntax_ref (inner)
idt}. This is the most basic category for variables in iterated binders,
such as ‹λ› or ‹∧›.
🚫 @{syntax_ref (inner) pttrn} and @{syntax_ref (inner) pttrns} denote
patterns for abstraction, cases bindings etc. In Pure, these categories
start as a merely copy of @{syntax (inner) idt} and @{syntax (inner) idts},
respectively. Object-logics may add additional productions for binding
forms.
🚫 @{syntax_ref (inner) type} denotes types of the meta-logic.
Here are some further explanations of certain syntax features.
▪ In @{syntax (inner) idts}, note that ‹x :: nat y› is parsed as ‹x :: (nat
y)›, treating ‹y› like a type constructor applied to ‹nat›. To avoid this
interpretation, write ‹(x :: nat) y› with explicit parentheses.
▪ Similarly, ‹x :: nat y :: nat› is parsed as ‹x :: (nat y :: nat)›. The
correct form is ‹(x :: nat) (y :: nat)›, or ‹(x :: nat) y :: nat› if ‹y› is
last in the sequence of identifiers.
▪ Type constraints for terms bind very weakly. For example, ‹x < y :: nat›
is normally parsed as ‹(x < y) :: nat›, unless ‹<\<close> has a very low priority,
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
(y :: nat)›.
▪ Dummy variables (written as underscore) may occur in different
roles.
🚫 A sort ``‹_›'' refers to a vacuous constraint for type variables, which
is effectively ignored in type-inference.
🚫 A type ``‹_›'' or ``‹_ :: sort›'' acts like an anonymous inference
parameter, which is filled-in according to the most general type produced
by the type-checking phase.
🚫 A bound ``‹_›'' refers to a vacuous abstraction, where the body does not
refer to the binding introduced here. As in the term term‹λx _. x›,
which is ‹α›-equivalent to ‹λx y. x›.
🚫 A free ``‹_›'' refers to an implicit outer binding. Higher definitional
packages usually allow forms like ‹f x _ = x›.
🚫 A schematic ``‹_›'' (within a term pattern, see \secref{sec:term-decls})
refers to an anonymous variable that is implicitly abstracted over its
context of locally bound variables. For example, this allows pattern
matching of ‹{x. f x = g x}› against ‹{x. _ = _}›, or even ‹{_. _ = _}› by
using both bound and schematic dummies.
🚫 The three literal dots ``▩‹...›'' may be also written as ellipsis symbol ▩‹…›. In both cases this refers to a special schematic variable, which is
bound in the context. This special term abbreviation works nicely with
calculational reasoning (\secref{sec:calculation}).
🚫▩‹CONST› ensures that the given identifier is treated as constant term,
and passed through the parse tree in fully internalized form. This is
particularly relevant for translation rules (\secref{sec:syn-trans}),
notably on the RHS.
🚫▩‹XCONST› is similar to ▩‹CONST›, but retains the constant name as given. Thisisonlyrelevanttotranslationrules(\secref{sec:syn-trans}),notably ontheLHS. \<close>
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
