Set Printing Existential Instances. Set Printing All. Goallet y:=0 in exists x:y=y, x = x. intros.
eexists.
rename y into z. unfold z at 1 2. (* should fail because the evar type depends on z *)
Fail clear z. Abort.
Messung V0.5
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
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 und die Messung sind noch experimentell.