From 4580a2b05a9354e9a5ec5085f1a4382f23619c6c Mon Sep 17 00:00:00 2001 From: ia0 Date: Tue, 11 Aug 2026 14:31:05 +0200 Subject: [PATCH] doc: fix typo in the doc example of List.lex This PR fixes in a typo in an example of the documentation of `List.lex`, namely removing a redundant `= false`. --- 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 c783c236e0d3..d99b37a6ff92 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -270,7 +270,7 @@ Compares lists lexicographically with respect to a comparison on their elements. The lexicographic order with respect to `lt` is: * `[].lex (b :: bs)` is `true` -* `as.lex [] = false` is `false` +* `as.lex []` is `false` * `(a :: as).lex (b :: bs)` is true if `lt a b` or `a == b` and `lex lt as bs` is true. -/ @[specialize]