Quelle bug_16482.v Sprache: Coq

Set Definitional UIP.
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.

Inductive eqn {A : Type} (x : A) : A -> SProp := refl : @eqn A x x.

Definition Rw {A B : Type} (e : eqn A B) (x : A) : B := match e with | refl _ => x end.

Definition F (A : Type) (P : A -> Type) (Q1 : forall x, P x): SProp.
Proof.
refine (eqn Q1 _).
intro a.
refine (Rw _ (Q1 a)).
reflexivity.
Defined.

Record BTy : Type := {
  typL : Type;
  typP : typL -> Type;
  typQ : forall x, typP x;
  eps : @F typL typP typQ;
}.
(* Anomaly "Uncaught exception Invalid_argument("index out of bounds")." *)

quality99%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

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.