|
(* Check that untypable beta-expansion are trapped *)
Variable A : nat -> Type.
Variable n : nat.
Variable P : forall m : nat, m = n -> Prop.
Goal forall p : n = n, P n p.
intro.
Fail pattern n, p.
Abort.
¤ Dauer der Verarbeitung: 0.16 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.
|
