Class Enc (A:Type) : Type :=
make_Enc { enc : A -> val }.
#[export] Hint Mode Enc + : typeclass_instances.
Parameter bar : forall A (EA:Enc A), EA = EA.
Parameter foo : forall (P:Prop),
P ->
P = P ->
True.
Parameter id : forall (P:Prop),
P -> P.
Check enc.
Lemma test : True.
eapply foo; [ eapply bar | apply id]. apply id. (* eapply bar introduces an unresolved typeclass evar that is no longer a candidate after the application (eapply should leave typeclass goals shelved). We ensure that this happens also _across_ goals in `[ | ]` and not only at `.`..
*) 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.
