text‹
index{datatypes!nested}% \S\ref{sec:nested-datatype} we defined the datatype of terms ›
datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list"
text‹\noindent
closed with the observation that the associated schema for the definition
primitive recursive functions leads to overly verbose definitions. Moreover,
you have worked exercise~\ref{ex:trev-trev} you will have noticed that
needed to declare essentially the same function as @{term"rev"}
prove many standard properties of list reversal all over again.
will now show you how \isacommand{recdef} can simplify
and proofs about nested recursive datatypes. As an example we
exercise~\ref{ex:trev-trev}: ›
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.
