Axiom R : Prop -> Prop -> Prop.
#[export] DeclareInstance R_refl : Reflexive R.
Class bar := { x : False }.
Record foo := { a : Prop ; b : bar }.
Definition default_foo (a0 : Prop) `{b : bar} : foo := {| a := a0 ; b := b |}.
Goalexists k, R k True. Proof.
eexists.
evar (b : bar). let e := matchgoalwith |- R ?e _ => constr:(e) end in
unify e (a (default_foo True)).
subst b. reflexivity. 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.
