Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: bug_4305.v Sprache: Coq

Original von: Coq^©

(* Call of apply on <-> failed because of evars in elimination predicate *)
Generalizable Variables patch.

Class Patch (patch : Type) := {
    commute : patch -> patch -> Prop
}.

Parameter flip : forall `{patchInstance : Patch patch}
                        {a b : patch},
                 commute a b <-> commute b a.

Lemma Foo : forall `{patchInstance : Patch patch}
                    {a b : patch},
            (commute a b)
         -> True.
Proof.
intros.
apply flip in H.

(* failed in well-formed arity check because elimination predicate of
   iff in (@flip _ _ _ _) had normalized evars while the ones in the
   type of (@flip _ _ _ _) itself had non-normalized evars *)

(* By the way, is the check necessary ? *)
Abort.

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.