Set Warnings "-uniform-inheritance". Set Printing All.
Module CS.
Structure foo := { sort :> Type; a : sort }.
Axiom T1 : Type -> Type. Axiom T2 : Type -> Type. Axiom x : T1 nat.
Module T1. Axiom f : forall A : foo, T1 (sort A) -> T2 nat.
#[canonical] Definition foo_nat := {| sort := nat; a := 1 |}.
Coercion f : T1 >-> T2. Check (x : T2 _). End T1.
Module T2. Axiom f : forall A : foo, T1 (sort A) -> T2 nat.
#[canonical] Definition foo_A A x := {| sort := A; a := x |}.
Coercion f : T1 >-> T2. Check (f _ x : T2 _). End T2.
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.
