Goalforall x : nat, x = x. Proof. intros x.
refine ((fun x x => _ tt) tt tt). let t := matchgoalwith [ |- ?P ] => P end in let _ := type of t in idtac. Abort.
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.
