|
Maybe[T:TYPE] : THEORY
BEGIN
Maybe: DATATYPE
BEGIN
None : none?
Some(val:T): some?
END Maybe
val2some(t:T) : MACRO Maybe = Some(t)
CONVERSION val2some
a : VAR Maybe
Maybe_none : LEMMA
none?(a) IFF
a = None
Maybe_some : LEMMA
some?(a) IMPLIES
EXISTS (t:T) : val(a) = t AND a = Some(t)
Maybe_or : LEMMA
none?(a) OR some?(a)
Maybe_either: LEMMA
a = None OR EXISTS (t:T) : val(a) = t AND a = Some(t)
END Maybe
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
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 ist noch experimentell.
|
