(* Title: Notation for hotel key card system Author:TobiasNipkow,TUMuenchen
*)
(*<*) theoryNotation imports"HOL-Library.LaTeXsugar" begin
abbreviation "SomeFloor" (‹(⌊_⌋)›) where"⌊x⌋≡ Some x" (*>*)
subsection‹Notation›
text‹
conforms largely to everyday mathematical notation.
section introduces further non-standard notation and in particular
few basic data types with their primitive operations.
sloppy
begin{description}
item[Types] The type of truth values is called @{typ bool}. The
of total functions is denoted by ‹==>›. Type variables
with a quote, as in @{typ"'a"}, @{typ"'b"} etc. The notation
t$~‹::›~$\tau$ means that term $t$ has type $\tau$.
item[Functions] can be updated at ‹x› with new value ‹y›,
@{term"f(x:=y)"}. The range of a function is @{term"range f"},
{prop"inj f"} means ‹f› is injective.
item[Pairs] come with the two projection functions ‹fst :: 'a × 'b ==> 'a› and ‹snd :: 'a × 'b ==> 'b›.
item[Sets] have type @{typ"'a set"}.
item[Lists] (type @{typ"'a list"}) come with the empty list
{term"[]"}, the infix constructor ‹⋅›, the infix ‹@›
appends two lists, and the conversion function @{term set} from
to sets. Variable names ending in ``s'' usually stand for
.
item[Records] are constructed like this ‹(f1 = v1, …)›
updated like this \mbox{‹r(fi := vi, …)›},
the ‹fi› are the field names, ‹vi› the values and ‹r› is a record.
end{description}\fussy ‹option› is defined like this
begin{center}
isacommand{datatype} ‹'a option = None | Some 'a›
end{center}
adjoins a new element @{term None} to a type @{typ 'a}. For
we write @{term"Some a"} instead of @{term[source]"Some a"}.
that ‹[A1; …; An]==> A› ‹A1==>…==> An==> A›, which is the same as
`If ‹A1› and \dots\ and ‹An› then ‹A›''. ›
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.
