Quelle bug_15403.v Sprache: Coq

Module Type EqType.
   Parameter Inline t : Type.
   Parameter eq : t -> t -> Prop.
End EqType.

Module NAT.
   Definition t := nat.
   Definition eq := @eq nat.
End NAT.

Module F (E:EqType) :=
  E.

Module Import NAT' := F NAT.

(* NAT'.eq should declared arguments in nat_scope *)
Notation "1" := true.
Check NAT'.eq 1 1.

quality98%

¤ Dauer der Verarbeitung: 0.3 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.