doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
changeset 8771 026f37a86ea7
parent 8749 2665170f104a
child 9145 9f7b8de5bfaf
equal deleted inserted replaced
8770:bfab4d4b7516 8771:026f37a86ea7
    52 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~else~valif~e~env){"}%
    52 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~else~valif~e~env){"}%
    53 \begin{isamarkuptext}%
    53 \begin{isamarkuptext}%
    54 \subsubsection{Transformation into and of If-expressions}
    54 \subsubsection{Transformation into and of If-expressions}
    55 
    55 
    56 The type \isa{boolex} is close to the customary representation of logical
    56 The type \isa{boolex} is close to the customary representation of logical
    57 formulae, whereas \isa{ifex} is designed for efficiency. Thus we need to
    57 formulae, whereas \isa{ifex} is designed for efficiency. It is easy to
    58 translate from \isa{boolex} into \isa{ifex}:%
    58 translate from \isa{boolex} into \isa{ifex}:%
    59 \end{isamarkuptext}%
    59 \end{isamarkuptext}%
    60 \isacommand{consts}~bool2if~::~{"}boolex~{\isasymRightarrow}~ifex{"}\isanewline
    60 \isacommand{consts}~bool2if~::~{"}boolex~{\isasymRightarrow}~ifex{"}\isanewline
    61 \isacommand{primrec}\isanewline
    61 \isacommand{primrec}\isanewline
    62 {"}bool2if~(Const~b)~=~CIF~b{"}\isanewline
    62 {"}bool2if~(Const~b)~=~CIF~b{"}\isanewline