docs: fix typo "an position" → "a position" in Coercions.lean#275
Open
linbo328 wants to merge 1 commit into
Open
docs: fix typo "an position" → "a position" in Coercions.lean#275linbo328 wants to merge 1 commit into
linbo328 wants to merge 1 commit into
Commits
Commits on May 13, 2026
- committed
Bounty Hunter Bot