Set Primitive Projections. SetImplicitArguments. Set Universe Polymorphism.
Inductive paths A (x : A) : A -> Type := idpath : paths x x.
Notation"x = y :> A" := (@paths A x y). Notation"x = y" := (x = y :> _).
Record foo := { x : Type; H : x = x }.
Create HintDb bar discriminated.
#[export] Hint Resolve H : bar. Goalforall y : foo, @x y = @x y. intro y.
progress autowith bar. (* failed to progress *) Abort.
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.
