max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: fix a typo in Pairwise doc (#9375)

Browse source 
doc: fix a typo in Pairwise doc

This PR fixes a sentence in the Pairwise doc in List/Basic
This commit is contained in:
Filippo A. E. Nuccio 2025-07-15 13:39:02 +02:00 • committed by GitHub
parent 6e9bc1359d
commit 08d8bed022
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/List/Basic.lean
View file

@ -1369,7 +1369,7 @@ Each element of a list is related to all later elements of the list by `R`.
`Pairwise R l` means that all the elements of `l` with earlier indexes are `R`-related to all the
elements with later indexes.
For example, `Pairwise (· ≠ ·) l` asserts that `l` has no duplicates, and if `Pairwise (· < ·) l`
For example, `Pairwise (· ≠ ·) l` asserts that `l` has no duplicates, and `Pairwise (· < ·) l`
asserts that `l` is (strictly) sorted.
Examples: