From 0167a185da544525bc938d4525c016e2e65b4e66 Mon Sep 17 00:00:00 2001 From: Bounty Hunter Bot Date: Wed, 13 May 2026 23:02:37 +0000 Subject: [PATCH] docs: fix typo an position -> a position in Coercions.lean Fixes #272 --- book/FPLean/TypeClasses/Coercions.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/book/FPLean/TypeClasses/Coercions.lean b/book/FPLean/TypeClasses/Coercions.lean index 892c8c8..1128f24 100644 --- a/book/FPLean/TypeClasses/Coercions.lean +++ b/book/FPLean/TypeClasses/Coercions.lean @@ -32,7 +32,7 @@ tag := "string-path-coercion" %%% In the {ref "handling-input"}[source code to {lit}`feline`], a {moduleName}`String` is converted to a {moduleName}`FilePath` using the anonymous constructor syntax. -In fact, this was not necessary: Lean defines a coercion from {moduleName}`String` to {moduleName}`FilePath`, so a string can be used in an position where a path is expected. +In fact, this was not necessary: Lean defines a coercion from {moduleName}`String` to {moduleName}`FilePath`, so a string can be used in a position where a path is expected. Even though the function {anchorTerm readFile}`IO.FS.readFile` has type {anchorTerm readFile}`System.FilePath → IO String`, the following code is accepted by Lean: ```anchor fileDumper