From 08d8bed02228d04256aa7c3ed176747aeb40fe50 Mon Sep 17 00:00:00 2001 From: "Filippo A. E. Nuccio" Date: Tue, 15 Jul 2025 13:39:02 +0200 Subject: [PATCH] doc: fix a typo in Pairwise doc (#9375) doc: fix a typo in Pairwise doc This PR fixes a sentence in the Pairwise doc in List/Basic --- src/Init/Data/List/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index aad728f5a8..f6fcd6c77c 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -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: