Skip to content

Commit 1335910

Browse files
fix: look up internal tags in freshTag deduplication
`Coe String Tag` made `tags.contains attempt` search for `Tag.provided`, so colliding auto-generated `Tag.internal` names were never detected. Fixes #897. Co-authored-by: Cursor <cursoragent@cursor.com>
1 parent 36a4465 commit 1335910

1 file changed

Lines changed: 3 additions & 1 deletion

File tree

src/verso-manual/VersoManual/Basic.lean

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -417,7 +417,9 @@ def freshTag [Monad m] [MonadStateOf TraverseState m] (hint : String) (id : Inte
417417
let mut numPart : Option Nat := none
418418
repeat
419419
let attempt := tagStr strPart numPart
420-
if (← get).tags.contains attempt then
420+
-- Lookup must use `Tag.internal`: `attempt` is a `String`, and the `Coe String Tag`
421+
-- instance would otherwise search for `Tag.provided`, so generated tags never collide.
422+
if (← get).tags.contains (Tag.internal attempt) then
421423
numPart := some <| numPart.map (· + 1) |>.getD 0
422424
else break
423425
let tag := tagStr strPart numPart

0 commit comments

Comments
 (0)