Quelle bug_7421.v Sprache: Coq

Universe i j.

Goal False.
Proof.
  Check Type@{i} : Type@{j}.
  Fail constr_eq_strict Type@{i} Type@{j}.
  assert_succeeds constr_eq Type@{i} Type@{j}. (* <- i=j is forgotten after assert_succeeds *)
  Fail constr_eq_strict Type@{i} Type@{j}.

  constr_eq Type@{i} Type@{j}. (* <- i=j is retained *)
  constr_eq_strict Type@{i} Type@{j}.
  Fail Check Type@{i} : Type@{j}.

  Fail constr_eq Prop Set.
  Fail constr_eq Prop Type.

  Fail constr_eq_strict Type Type.
  constr_eq Type Type.

  constr_eq_strict Set Set.
  constr_eq Set Set.
  constr_eq Prop Prop.

  let x := constr:(Type) in constr_eq_strict x x.
  let x := constr:(Type) in constr_eq x x.

  Fail lazymatch type of prod with
       | ?A -> ?B -> _ => constr_eq_strict A B
       end.
  lazymatch type of prod with
  | ?A -> ?B -> _ => constr_eq A B
  end.
  lazymatch type of prod with
  | ?A -> ?B -> ?C => constr_eq A C
  end.

Abort.

quality100%

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