Skip to content

Commit c632a0a

Browse files
authored
doc: fix typo in the doc example of List.lex (#14987)
This PR fixes in a typo in an example of the documentation of `List.lex`, namely removing a redundant `= false`.
1 parent 6778cc8 commit c632a0a

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

src/Init/Data/List/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -270,7 +270,7 @@ Compares lists lexicographically with respect to a comparison on their elements.
270270
271271
The lexicographic order with respect to `lt` is:
272272
* `[].lex (b :: bs)` is `true`
273-
* `as.lex [] = false` is `false`
273+
* `as.lex []` is `false`
274274
* `(a :: as).lex (b :: bs)` is true if `lt a b` or `a == b` and `lex lt as bs` is true.
275275
-/
276276
@[specialize]

0 commit comments

Comments
 (0)