TimeM's `✓` tick breaks when HasWellFormed is imported

Cslib's own ✓ notations conflict with each other: TimeM's tick, a leading do-element macro, is captured by HasWellFormed's global postfix whenever both are imported. The practical effect is that the documented TimeM syntax works when importing the module on its own and silently breaks for anyone who imports Cslib as a whole. This is the same class of problem as #631 (a global notation without a whitespace guard reaching across line breaks).

The problem

Two notations share the ✓ token:

-- Cslib/Algorithms/Lean/TimeM.lean
macro "✓" body:doElem : doElem => `(doElem| ✓[1] $body)

-- Cslib/Foundations/Syntax/HasWellFormed.lean
notation x:max "✓" => HasWellFormed.wf x

The second one is global and has no whitespace guard, so with both in scope the parser does not stop at the end of the do item before the tick: it sees the ✓ on the next line and reads it as the postfix applied to the previous expression. The tick is consumed, and the errors land on the line above it, which makes this quite hard to diagnose.

MWE

import Cslib.Algorithms.Lean.TimeM

open Cslib.Algorithms.Lean in
def f (n : Nat) : TimeM Nat Nat := do
  let m := n
  ✓ return m

This compiles. Add import Cslib.Foundations.Syntax.HasWellFormed (or just use import Cslib) and it fails with

error: failed to synthesize instance of type class Cslib.HasWellFormed ℕ   -- on the `let m := n` line
error: Application type mismatch: m has type Prop but is expected to have type ℕ

because let m := n has become let m := n✓, i.e. HasWellFormed.wf n : Prop.

How I encountered this

I ran into this with the treap exercise from the Theoretical Computer Science Proving in Lean challenge in the ICML 2026 AI for Math workshop. The challenge's TreapLogic task file implements treap split and merge, instrumented with TimeM to count operations, and uses the tick exactly as documented:

def mergeT (l r : TreapNode Key Prio) : TimeM ℕ (TreapNode Key Prio) := do
  match l, r with
  ...
  | BinaryTree.node kp_1 l_1 r_1, BinaryTree.node kp_2 l_2 r_2 =>
    if kp_1.prio ≥ kp_2.prio then
      ...
    else
      let new_l ← mergeT (BinaryTree.node kp_1 l_1 r_1) l_2
      let new_r := r_2
      ✓ return (BinaryTree.node kp_2 new_l new_r)

The file compiles with import Cslib.Algorithms.Lean.TimeM alone. With import Cslib it fails with two errors. On the let new_r := r_2 line, Lean reports failed to synthesize Cslib.HasWellFormed (BinaryTree (KeyPrioPair Key Prio)): the postfix has consumed the tick from the line below, so the binding is really parsed as let new_r := r_2✓, i.e. HasWellFormed.wf r_2, which makes new_r a Prop instead of the intended BinaryTree (KeyPrioPair Key Prio). The return line below then fails with a type mismatch, because BinaryTree.node kp_2 new_l new_r expects new_r to be that tree — which it would have been, had the binding not been rewritten. Both messages point at code that is correct as written, which makes this hard to diagnose.

Two workarounds exist. Replacing ✓ with ✓[1] is the reliable one, since ✓[ is a longer token and is not captured by the postfix. Reordering the do block so that a let x ← e bind sits directly above the tick also works, because an arrow-bind's right-hand side ends at the line break — though this is fragile and easy to break again when editing. Either way, the documented short form should work as written.

Possible fixes

There are a few ways this could be addressed:

• Declare the HasWellFormed postfix as scoped (it is the intruding side; TimeM's macros only fire in do-element position).
• Rename one of the two, as #393 did for the context-fill notation (c[t] → c<[t]).
• Give the postfix a whitespace guard so it cannot reach across line breaks.

Once it's decided how to fix this, I would be happy to make a PR.

Environment

• Reproduced on current main (d6c0b90, 2026-06-12, toolchain v4.31.0-rc2): the MWE and the treap example both compile with the TimeM import alone and fail with HasWellFormed in scope.

Start by comparing the notation declarations in Cslib/Algorithms/Lean/TimeM.lean and Cslib/Foundations/Syntax/HasWellFormed.lean, then reproduce the MWE with each import combination. Decide among scoping, renaming, or a whitespace guard, and verify that the documented short-form tick compiles with the full Cslib import.