Quellcode-Bibliothek bug_20188.v

Sprache: Coq

Require Import 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 ].

Messung V0.5 in Prozent

¤ 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.0.11Bemerkung: (vorverarbeitet am 2026-06-04) ¤

Wurzel

Suchen

PVS Prover

Isabelle Prover

NIST Cobol Testsuite

Cephes Mathematical Library

Vienna Development Method

Bemerkung:

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.