Quelle bug_20115.v Sprache: Coq

Module Type PARAM.
Parameter T : Type.
End PARAM.

Module Type NESTED.
  Declare Module KI: PARAM.
End NESTED.

Module Type BUNDLE.
  Declare Module KI: PARAM.
  Declare Module K0: NESTED with Module KI := KI.
End BUNDLE.

Declare Module MyKI : PARAM.
Declare Module MyKO : BUNDLE with Module KI := MyKI.

(** Check that the delta-resolver contains the correct equivalence

    MyKO.K0.KI.T ↦ MyKI.T *)

Goal MyKI.T.
Proof.
match goal with
[ |- MyKO.K0.KI.T ] => idtac
end.
Abort.

Goal MyKO.K0.KI.T.
Proof.
match goal with
[ |- MyKI.T ] => idtac
end.
Abort.

quality99%

¤ Dauer der Verarbeitung: 0.4 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.