|
(* Check that Match arguments are forbidden *)
Ltac E x := apply x.
Goal True -> True.
Fail E ltac:(match goal with
| |- _ => intro H
end).
Abort.
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
