doc-src/TutorialI/fp.tex
changeset 27712 007a339b9e7d
parent 27015 f8537d69f514
child 44048 64f574163ca2
equal deleted 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