Quelle bug_4628.v Sprache: Coq

Module first.
  Polymorphic Record BAR (A:Type) :=
  { foo: A->Prop; bar: forall (x y: A), foo x -> foo y}.

Section A.
Context {A:Type}.

Set Printing Universes.

Hint Resolve bar.
Goal forall (P:BAR A) x y, foo _ P x -> foo _ P y.
intros.
eauto.
Qed.
End A.
End first.

Module firstbest.
  Polymorphic Record BAR (A:Type) :=
  { foo: A->Prop; bar: forall (x y: A), foo x -> foo y}.

Section A.
Context {A:Type}.

Set Printing Universes.

Polymorphic Hint Resolve bar.
Goal forall (P:BAR A) x y, foo _ P x -> foo _ P y.
intros.
eauto.
Qed.
End A.
End firstbest.

Module second.
Axiom foo: Set.
Axiom foo': Set.

Polymorphic Record BAR (A:Type) :=
  { bar: foo' -> foo}.
Set Printing Universes.

Lemma baz@{i}: forall (P:BAR@{Set} nat), foo' -> foo.
  eauto using bar.
Qed.
End second.

quality99%

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