test(Syntax): add regression test for well-formed notation collision

Author: litholight

CslibTests.lean

@@ -11,3 +11,4 @@ import CslibTests.LTS
 import CslibTests.LambdaCalculus
 import CslibTests.MLL
 import CslibTests.Reduction
+import CslibTests.HasWellFormed

CslibTests/HasWellFormed.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2026 Sean D. Stoneburner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sean D. Stoneburner
+-/
+import Cslib.Algorithms.Lean.TimeM
+import Cslib.Foundations.Syntax.HasWellFormed
+
+open Cslib.Algorithms.Lean
+
+/-!
+# Syntax Collision Test
+This file tests that the `✓` prefix macro from `TimeM` does not collide with
+the `✓` postfix notation from `HasWellFormed` across line breaks.
+-/
+
+def testParserCollision (n : Nat) : TimeM Nat Nat := do
+  let m := n
+  ✓ return m
+
+-- Ensure the postfix notation still functions correctly when attached without whitespace
+variable {α : Type*} [Cslib.HasWellFormed α] (x : α)
+#check x✓