[Typo] Section 3.6.1, "an position"

[jlebar]

In fact, this was not necessary: Lean defines a coercion from String to FilePath, so a string can be used in an position where a path is expected.

Should be "a position".