Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: bug_1322.v Sprache: Coq

Original von: Coq^©

Require Import Setoid.

Section transition_gen.

Variable I : Type.
Variable I_eq :I -> I -> Prop.
Variable I_eq_equiv : Setoid_Theory I I_eq.

(* Add Relation I I_eq
  reflexivity proved by I_eq_equiv.(Seq_refl I I_eq)
  symmetry proved by I_eq_equiv.(Seq_sym I I_eq)
  transitivity proved by I_eq_equiv.(Seq_trans I I_eq)
as I_eq_relation. *)

Add Parametric Relation : I I_eq
  reflexivity  proved by I_eq_equiv.(@Equivalence_Reflexive _ _)
  symmetry     proved by I_eq_equiv.(@Equivalence_Symmetric _ _)
  transitivity proved by I_eq_equiv.(@Equivalence_Transitive _ _)
  as I_with_eq.

Variable F : I -> Type.
Variable F_morphism : forall i j, I_eq i j -> F i = F j.

Add Morphism F with signature I_eq ==> (@eq _) as F_morphism2.
Admitted.

End transition_gen.

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.