Quelle bug_16140.v Sprache: Coq

(* Test regression https://github.com/coq/coq/issues/16140
   where congruence produces ill-typed terms *)

Inductive wrap1 : Type :=
  wrap1I (u : unit) : match u with tt => bool end -> wrap1.

Goal (wrap1I tt false) = (wrap1I tt true) -> False.
Proof.
  Fail congruence. (* expected to fail *)
Abort.

Inductive wrap2 : unit -> Type :=
  wrap2I (u : unit) : match u with tt => bool end -> wrap2 u.

Goal (wrap2I tt false) = (wrap2I tt true) -> False.
Proof.
  Fail congruence. (* expected to fail *)
Abort.

Inductive wrap3 (u : unit) : Type :=
  wrap3I : match u with tt => bool end -> wrap3 u.

Goal (wrap3I tt false) = (wrap3I tt true) -> False.
Proof.
  congruence.
Qed.

quality100%

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