Quelle pairs2.thy

Sprache: Isabelle

(*<*)
theory pairs2 imports Main begin
(*>*)
text‹\label{sec:pairs}\index{pairs and tuples}
also has ordered pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type
\tau@i$. The functions \cdx{fst} and
cdx{snd} extract the components of a pair:
\isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands
\isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for
\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have
isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.

:
begin{itemize}
item
is also the type \tydx{unit}, which contains exactly one
denoted by~\cdx{()}. This type can be viewed
a degenerate product with 0 components.
item
, like type 🍋‹nat›, are datatypes, which means
particular that ‹induct_tac› and ‹case_tac› are applicable to
of product type.
split the term into a number of variables corresponding to the tuple structure
up to 7 components).
item
with more than two or three components become unwieldy;
are preferable.
end{itemize}
more information on pairs and records see Chapter~\ref{ch:more-types}.
›
(*<*)
end
(*>*)

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.