Set Warnings "-uniform-inheritance". Set Printing All.
Module TC.
Class foo (A : Type) := { a : A }.
#[local] Hint Mode foo + : typeclass_instances.
#[local] Instance bool_foo : foo bool := {| a := true |}.
#[local] Instance nat_foo : foo nat := {| a := 1 |}.
#[local] Instance pair_foo A B : foo A -> foo B -> foo (A * B) := fun x y => {| a := (a,a) |}.
Axiom T1 : Type -> Type. Axiom T2 : Type -> Type. Axiom x : T1 nat.
Module T1. Axiom f : forall A, foo (A * bool) -> T1 A -> T2 nat.
Coercion f : T1 >-> T2. Check (x : T2 _). End T1.
Module T2. Axiom f : forall A, foo A -> T1 nat -> T2 A.
Coercion f : T1 >-> T2. Check (x : T2 _). Check (x : T2 bool). 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.
