|
Require Import RelationClasses.
Axiom R : Prop -> Prop -> Prop.
Declare Instance 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 |}.
Goal exists k, R k True.
Proof.
eexists.
evar (b : bar).
let e := match goal with |- R ?e _ => constr:(e) end in
unify e (a (default_foo True)).
subst b.
reflexivity.
Abort.
¤ Dauer der Verarbeitung: 0.31 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.
|
