Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: st122a.cob Sprache: Coq

Original von: Coq^©

Set Universe Polymorphism.
Set Primitive Projections.

Axiom Ω : Type.

Record Pack (A : Ω -> Type) (Aᴿ : Ω -> (forall ω : Ω, A ω) -> Type) := mkPack {
  elt : forall ω, A ω;
  prp : forall ω, Aᴿ ω elt;
}.

Record TYPE := mkTYPE {
  wit : Ω -> Type;
  rel : Ω -> (forall ω : Ω, wit ω) -> Type;
}.

Definition El (A : TYPE) : Type := Pack A.(wit) A.(rel).

Definition Typeᶠ : TYPE := {|
  wit := fun _ => Type;
  rel := fun _ A => (forall ω : Ω, A ω) -> Type;
                          |}.
Set Printing Universes.
Fail Definition Typeᵇ : El Typeᶠ :=
  mkPack _ _ (fun w => Type) (fun w A => (forall ω, A ω) -> Type).

Definition Typeᵇ : El Typeᶠ :=
  mkPack _ (fun _ (A : Ω -> Type) => (forall ω : Ω, A ω) -> _) (fun w => Type) (fun w A => (forall ω, A ω) -> Type).

(** Bidirectional typechecking helps here *)
Require Import Program.Tactics.
Program Definition progTypeᵇ : El Typeᶠ :=
  mkPack _ _ (fun w => Type) (fun w A => (forall ω, A ω) -> Type).

(**
The command has indeed failed with message:
Error: Conversion test raised an anomaly
**)

Definition Typeᵇ' : El Typeᶠ.
Proof.
unshelve refine (mkPack _ _ _ _).
+ refine (fun _ => Type).
+ simpl. refine (fun _ A => (forall ω, A ω) -> Type).
Defined.

¤ Dauer der Verarbeitung: 0.77 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

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.