Skip to content

Commit caae86f

Browse files
committed
Typo fix
1 parent 1e9814e commit caae86f

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

MathlibTest/DifferentialGeometry/Notation.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -544,7 +544,7 @@ variable [IsManifold I 1 M] [IsManifold I' 1 M']
544544
-- TODO: can there be better error messages when forgetting the smoothness exponent?
545545
section error
546546

547-
-- yields a parse error, "unexpected toekn '/--'; expected term"
547+
-- yields a parse error, "unexpected token '/--'; expected term"
548548
-- #check CMDiffAt[s] f
549549

550550
/--

0 commit comments

Comments
 (0)