|
Module Type ELEM.
Parameter A : Set.
Parameter x : A.
End ELEM.
Module Nat.
Definition A := nat.
Definition x := 0.
End Nat.
Module List (X: ELEM).
Inductive list : Set :=
| nil : list
| cons : X.A -> list -> list.
Definition head (l : list) := match l with
| nil => X.x
| cons x _ => x
end.
Definition singl (x : X.A) := cons x nil.
Lemma head_singl : forall x : X.A, head (singl x) = x.
auto.
Qed.
End List.
Module N := List Nat.
¤ Dauer der Verarbeitung: 0.0 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.
|
