Skip to content

Commit

Permalink
fix: a small mistake (strings -> arrays) (#226)
Browse files Browse the repository at this point in the history
  • Loading branch information
eyelash authored Jan 7, 2025
1 parent 1cef14d commit 5d470a6
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Manual/BasicTypes/Array.lean
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ The {lean}`Array` type represents sequences of elements, addressable by their po
Arrays are specially supported by Lean:
* They have a _logical model_ that specifies their behavior in terms of lists of elements, which specifies the meaning of each operation on arrays.
* They have an optimized run-time representation in compiled code as {tech}[dynamic arrays], and the Lean runtime specially optimizes array operations.
* There is {ref "array-syntax"}[array literal syntax] for writing strings.
* There is {ref "array-syntax"}[array literal syntax] for writing arrays.

Arrays can be vastly more efficient than lists or other sequences in compiled code.
In part, this is because they offer good locality: because all the elements of the sequence are next to each other in memory, the processor's caches can be used efficiently.
Expand Down

0 comments on commit 5d470a6

Please sign in to comment.