|
(* Classes and sections *)
Section OPT.
Variable A: Type.
Inductive MyOption: Type :=
| MyNone: MyOption
| MySome: A -> MyOption.
Class Opt: Type := {
f_opt: A -> MyOption
}.
End OPT.
Definition f_nat (n: nat): MyOption nat := MySome _ n.
Instance Nat_Opt: Opt nat := {
f_opt := f_nat
}.
¤ Dauer der Verarbeitung: 0.15 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.
|
