text‹A handy abbreviation when working with maps› abbreviation make_map :: "'a set ==> 'b ==> ('a ⇀ 'b)" (‹[ _ |=> _ ]›) where "[ks |=> v] ≡ λk. if k ∈ ks then Some v else None"
text‹Projecting the components of a triple› definition"fst3 ≡ fst" definition"snd3 ≡ fst ∘ snd" definition"thd3 ≡ snd ∘ snd"
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.
