Skip to content

Commit febad6a

Browse files
authored
doc: typo in IO.lean (#8657)
1 parent 257cd15 commit febad6a

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Init/System/IO.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -567,7 +567,7 @@ def addHeartbeats (count : Nat) : BaseIO Unit := do
567567
/--
568568
Whether a file should be opened for reading, writing, creation and writing, or appending.
569569
570-
A the operating system level, this translates to the mode of a file handle (i.e., a set of `open`
570+
At the operating system level, this translates to the mode of a file handle (i.e., a set of `open`
571571
flags and an `fdopen` mode).
572572
573573
None of the modes represented by this datatype translate line endings (i.e. `O_BINARY` on Windows).

0 commit comments

Comments
 (0)