\newcommand {\as }{\kw {as}}\newcommand {\case }{\kw {case}}\newcommand {\cons }{\textsf {cons}}\newcommand {\consf }{\textsf {consf}}\newcommand {\emptyf }{\textsf {emptyf}}\newcommand {\End }{\kw {End}}\newcommand {\kwend }{\kw {end}}\newcommand {\even }{\textsf {even}}\newcommand {\evenO }{\textsf {even}_\textsf {O}}\newcommand {\evenS }{\textsf {even}_\textsf {S}}\newcommand {\Fix }{\kw {Fix}}\newcommand {\fix }{\kw {fix}}\newcommand {\for }{\textsf {for}}\newcommand {\forest }{\textsf {forest}}\newcommand {\Functor }{\kw {Functor}}\newcommand {\In }{\kw {in}}\newcommand {\ind }[3]{\kw {Ind}~[#1]\left (#2\mathrm {~:=~}#3\right )}\newcommand {\Indp }[4]{\kw {Ind}_{#4}[#1](#2:=#3)}\newcommand {\Indpstr }[5]{\kw {Ind}_{#4}[#1](#2:=#3)/{#5}}\newcommand {\injective }{\kw {injective}}\newcommand {\kw }[1]{\textsf {#1}}\newcommand {\length }{\textsf {length}}\newcommand {\letin }[3]{\kw {let}~#1:=#2~\kw {in}~#3}\newcommand {\List }{\textsf {list}}\newcommand {\lra }{\longrightarrow }\newcommand {\Match }{\kw {match}}\newcommand {\Mod }[3]{{\kw {Mod}}({#1}:{#2}\, \zeroone {:={#3}})}\newcommand {\ModImp }[3]{{\kw {Mod}}({#1}:{#2}:={#3})}\newcommand {\ModA }[2]{{\kw {ModA}}({#1}=={#2})}\newcommand {\ModS }[2]{{\kw {Mod}}({#1}:{#2})}\newcommand {\ModType }[2]{{\kw {ModType}}({#1}:={#2})}\newcommand {\mto }{.\; }\newcommand {\nat }{\textsf {nat}}\newcommand {\Nil }{\textsf {nil}}\newcommand {\nilhl }{\textsf {nil\_ hl}}\newcommand {\nO }{\textsf {O}}\newcommand {\node }{\textsf {node}}\newcommand {\nS }{\textsf {S}}\newcommand {\odd }{\textsf {odd}}\newcommand {\oddS }{\textsf {odd}_\textsf {S}}\newcommand {\ovl }[1]{\overline {#1}}\newcommand {\Pair }{\textsf {pair}}\newcommand {\plus }{\mathsf {plus}}\newcommand {\SProp }{\textsf {SProp}}\newcommand {\Prop }{\textsf {Prop}}\newcommand {\return }{\kw {return}}\newcommand {\Set }{\textsf {Set}}\newcommand {\Sort }{\mathcal {S}}\newcommand {\Str }{\textsf {Stream}}\newcommand {\Struct }{\kw {Struct}}\newcommand {\subst }[3]{#1\{ #2/#3\} }\newcommand {\tl }{\textsf {tl}}\newcommand {\tree }{\textsf {tree}}\newcommand {\trii }{\triangleright_ \iota }\newcommand {\Type }{\textsf {Type}}\newcommand {\WEV }[3]{\mbox {$#1[] \vdash #2 \lra #3$}}\newcommand {\WEVT }[3]{\mbox {$#1[] \vdash #2 \lra $}\\ \mbox {$ #3$}}\newcommand {\WF }[2]{{\mathcal {W\! F}}(#1)[#2]}\newcommand {\WFE }[1]{\WF {E}{#1}}\newcommand {\WFT }[2]{#1[] \vdash {\mathcal {W\! F}}(#2)}\newcommand {\WFTWOLINES }[2]{{\mathcal {W\! F}}\begin {array}{l}(#1)\\ \mbox {}[{#2}]\end {array}}\newcommand {\with }{\kw {with}}\newcommand {\WS }[3]{#1[] \vdash #2 <: #3}\newcommand {\WSE }[2]{\WS {E}{#1}{#2}}\newcommand {\WT }[4]{#1[#2] \vdash #3 : #4}\newcommand {\WTE }[3]{\WT {E}{#1}{#2}{#3}}\newcommand {\WTEG }[2]{\WTE {\Gamma }{#1}{#2}}\newcommand {\WTM }[3]{\WT {#1}{}{#2}{#3}}\newcommand {\zeroone }[1]{[{#1}]}quality 100%
¤ Dauer der Verarbeitung: 0.4 Sekunden
¤ *© Formatika GbR, Deutschland
