Lemma foo : True. Proof.
unshelve refine (let x : Type := _ in _).
refine (list _).
exact_no_check 0.
Fail matchgoalwith x := ?v |- _ => let _ := type of v in idtacend. (* typing *) exact I.
Fail Qed. (* kernel *) 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.
