Quelle bug_17295.v Sprache: Coq

Require Import Setoid.

Set Printing Existential Instances.

Axiom A : Type.
Axiom i : A.
Axiom Equal : A -> A -> Prop.
Axiom P : A -> Prop.

Axiom everything_equal : forall (j : A), Equal i j.

Instance b : Morphisms.Proper (Equal ==> Basics.impl) P. Admitted.

Axiom forget : P i -> A.

Lemma blah (H : P i) : True.
unshelve rewrite everything_equal in H.
Fail exact (forget H).
Abort.

Lemma blah (H : P i) : True.
unshelve setoid_rewrite everything_equal in H.
Fail exact (forget H).
Abort.

quality100%

¤ Dauer der Verarbeitung: 0.6 Sekunden ¤

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.