Skip to content

Commit

Permalink
doc: fix typo in USize.size docstring (#3664)
Browse files Browse the repository at this point in the history
  • Loading branch information
casavaca authored Mar 13, 2024
1 parent 6004128 commit e61d082
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Init/Prelude.lean
Original file line number Diff line number Diff line change
Expand Up @@ -2036,7 +2036,7 @@ instance : Inhabited UInt64 where
default := UInt64.ofNatCore 0 (by decide)

/--
The size of type `UInt16`, that is, `2^System.Platform.numBits`, which may
The size of type `USize`, that is, `2^System.Platform.numBits`, which may
be either `2^32` or `2^64` depending on the platform's architecture.
Remark: we define `USize.size` using `(2^numBits - 1) + 1` to ensure the
Expand Down

0 comments on commit e61d082

Please sign in to comment.