Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: bug_3284.v Sprache: Coq

Original von: Coq^©

Generalizable Variables A.
Class Test A := { test : A }.

Lemma mylemma : forall `{Test A}, test = test.
Admitted. (* works fine *)

Definition mylemma' := forall `{Test A}, test = test.
About mylemma'.

¤ Dauer der Verarbeitung: 0.24 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

schauen Sie vor die Tür

Fenster

Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.