products/Sources/formale Sprachen/Isabelle/Doc/Tutorial/Misc image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei:   Sprache: Isabelle

Untersuchung Isabelle©

(*<*)
theory pairs2 imports Main begin
(*>*)
text\<open>\label{sec:pairs}\index{pairs and tuples}
HOL 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
are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands
for \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$}.

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

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.26Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤





zum Wurzelverzeichnis wechseln
Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen. Man kann per Verzeichnistruktur darin navigieren. Der Code wird farblich markiert angezeigt.
zum Wurzelverzeichnis wechseln
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Laden

Fehler beim Verzeichnis:


in der Quellcodebibliothek suchen

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff