Class A (n : nat) := {}. Definition three := 3.
#[export] Instance A_three : A three := {}. Definition three' := if true then three else 1. (* 1 *) Goal A (if true then three else 1). apply _. Qed.
#[export] HintOpaque three : typeclass_instances. (* 2 *) Goal A (if true then three else 1). apply _. Qed. (* 3 *) Goal A (three'). apply _. Qed.
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.
