Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: nc251a.cob 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.0 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht 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.