Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: diffs-coqtop-on.png Sprache: Coq

Original von: Coq^©

Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from original input, then from 3329 lines to 153 lines, then from 118 lines to 49 lines, then from 55 lines to 38 lines, then from 46 lines to 16 lines *)

Generalizable All Variables.
Set Universe Polymorphism.
Class Foo (A : Type) := {}.
Definition Baz := Foo.
Definition Bar {A B} `{Foo A, Foo B} : True.
Proof.
  Set Printing Universes.
  (* [change] should give fresh universes for each [Foo] *)
  change Foo with Baz in *.
  admit.
Defined.
Definition foo := @Bar nat.
Check @foo Set.
(* Toplevel input, characters 26-29:
Error:
The term "Set" has type "Type (* Set+1 *)
"Set" (Universe inconsistency: Cannot enforce Set < Set because Set = Set)). *)

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des 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.