|
Goal False.
intuition
match goal with
| |- _ => idtac " foo"
end.
lazymatch goal with _ => idtac end.
match goal with _ => idtac end.
unshelve lazymatch goal with _ => idtac end.
unshelve match goal with _ => idtac end.
unshelve (let x := I in idtac).
Abort.
Require Import ssreflect.
Goal True.
match goal with _ => idtac end => //.
Qed.
¤ Dauer der Verarbeitung: 0.0 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.
|
