Skip to content

Commit 34b237a

Browse files
authored
doc: fix typo in Inductive Types (#871)
1 parent 89f3a9d commit 34b237a

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Manual/Language/InductiveTypes.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -370,7 +370,7 @@ Not every inductive type is represented as indicated here—some inductive types
370370
axiom α : Prop
371371
```
372372

373-
* The representation of the fixed-width integer types {lean}`UInt8`, …, {lean}`UInt64`, {lean}`Int8`, …, {lean}`Int64`, and {lean}`USize` depends on the whether the code is compiled for a 32- or 64-bit architecture.
373+
* The representation of the fixed-width integer types {lean}`UInt8`, …, {lean}`UInt64`, {lean}`Int8`, …, {lean}`Int64`, and {lean}`USize` depends on whether the code is compiled for a 32- or 64-bit architecture.
374374
Their representation is described {ref "fixed-int-runtime"}[in a dedicated section].
375375

376376
* {lean}`Char` is represented by `uint32_t`. Because {lean}`Char` values never require more than 21 bits, they are always unboxed.

0 commit comments

Comments
 (0)