Set Primitive Projections. Classtype (t : Type) : Type :=
{ bar : t -> Prop }.
#[export] Instance type_nat : type nat :=
{ bar := fun _ => True }.
Definition foo_bar {n : nat} : bar n := I.
#[local] Hint Resolve (@foo_bar) : typeclass_instances.
#[local] Hint Resolve I : typeclass_instances. Checkltac:(typeclasses eauto with nocore typeclass_instances) : True. Checkltac:(typeclasses eauto with nocore typeclass_instances foo) : bar _.
Existing Class bar. Checkltac:(typeclasses eauto with nocore typeclass_instances foo) : bar _.
#[local] Hint Resolve (@foo_bar) : foo. Checkltac:(typeclasses eauto with nocore typeclass_instances foo) : bar _.
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.
