|
Class abstract_term {T} (x : T) := by_abstract_term : T.
Hint Extern 0 (@abstract_term ?T ?x) => change T; abstract (exact x) : typeclass_instances.
Goal True.
let term := constr:(I) in
let T := type of term in
let x := constr:((_ : abstract_term term) : T) in
let x := match constr:(x) with ?y => y end in
pose x as v. (* was Error: Variable x should be bound to a term but is bound to a constr. *)
exact v.
Qed.
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
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.
|
