equal
deleted
inserted
replaced
398 |
398 |
399 \input{Datatype/document/Fundata.tex} |
399 \input{Datatype/document/Fundata.tex} |
400 \bigskip |
400 \bigskip |
401 |
401 |
402 If you need nested recursion on the left of a function arrow, there are |
402 If you need nested recursion on the left of a function arrow, there are |
403 alternatives to pure HOL: LCF~\cite{paulson87} is a logic where types like |
403 alternatives to pure HOL\@. In the Logic for Computable Functions |
|
404 (LCF), types like |
404 \begin{isabelle} |
405 \begin{isabelle} |
405 \isacommand{datatype} lam = C "lam \isasymrightarrow\ lam" |
406 \isacommand{datatype} lam = C "lam \isasymrightarrow\ lam" |
406 \end{isabelle} |
407 \end{isabelle} |
407 do indeed make sense. Note the different arrow, |
408 do indeed make sense~\cite{paulson87}. Note the different arrow, |
408 \isa{\isasymrightarrow} instead of \isa{\isasymRightarrow}, |
409 \isa{\isasymrightarrow} instead of \isa{\isasymRightarrow}, |
409 expressing the type of \emph{continuous} functions. |
410 expressing the type of \emph{continuous} functions. |
410 There is even a version of LCF on top of HOL, |
411 There is even a version of LCF on top of HOL, |
411 called HOLCF~\cite{MuellerNvOS99}. |
412 called HOLCF~\cite{MuellerNvOS99}. |
412 |
413 |