Quelle bug_20537.v Sprache: unbekannt

Module M.
Tactic Notation (at level 5) "foo" int(x) := do x apply S; exact 0.
End M.

Import M.
(* Anomaly
"Uncaught exception Failure("Grammar.extend: No level labelled \"5\" in entry \"ltac_expr\"")."
*)

Check eq_refl : ltac:(foo 4) = 4.

Messung V0.5 in Prozent

Quelle bug_20537.v Sprache: unbekannt

[Dauer der Verarbeitung: 0.18 Sekunden, vorverarbeitet 2026-09-29]