RequireImport Ltac2.Ltac2. Notation"[[ x ]]" := ltac2:(()) (only parsing). Notation"[ x ]" := ltac2:(let x := Ltac2.Constr.pretype x in exact $x) (only parsing).
Fail Check foo. (* Error: The reference foo was not found in the current environment. *) Check [[ foo ]]. (* success *) Check [ foo ].
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 und die Messung sind noch experimentell.
