|
(* -*- coq-prog-args: ("-noinit"); -*- *)
Unset Elimination Schemes.
Module Type S.
Inductive foo : Prop :=.
Definition bar (x:foo) : Prop := match x with end.
End S.
Module M.
Inductive foo : Prop :=.
Definition bar (x:foo) : Prop := match x with end.
End M.
Module MS : S := M.
Module F (Z:S) := Z.
Module MS' : S := F M.
¤ Dauer der Verarbeitung: 0.18 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.
|
