doc-src/TutorialI/fp.tex
 changeset 27712 007a339b9e7d parent 27015 f8537d69f514 child 44048 64f574163ca2
equal inserted replaced
27711:5052736b8bcc 27712:007a339b9e7d
   138 Also available are higher-order functions like \isa{map} and \isa{filter}.
   138 Also available are higher-order functions like \isa{map} and \isa{filter}.
   139 Theory \isa{List} also contains
   139 Theory \isa{List} also contains
   140 more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates
   140 more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates
   141 $x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}.  In the rest of the tutorial we
   141 $x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}.  In the rest of the tutorial we
   142 always use HOL's predefined lists by building on theory \isa{Main}.
   142 always use HOL's predefined lists by building on theory \isa{Main}.

   143 \begin{warn}

   144 Looking ahead to sets and quanifiers in Part II:

   145 The best way to express that some element \isa{x} is in a list \isa{xs} is

   146 \isa{x $\in$ set xs}, where \isa{set} is a function that turns a list into the

   147 set of its elements.

   148 By the same device you can also write bounded quantifiers like

   149 \isa{$\forall$x $\in$ set xs} or embed lists in other set expressions.

   150 \end{warn}
   143
   151
   144
   152
   145 \subsection{The General Format}
   153 \subsection{The General Format}
   146 \label{sec:general-datatype}
   154 \label{sec:general-datatype}
   147
   155