commit: c632a0a0e434a951cdcf61bb4da3344abadd5587

[log]
author: Julien Cretin <git@ia0.eu>

Wed Sep 02 03:04:47 2026 +0000
committer: GitHub <noreply@github.com>

Wed Sep 02 03:04:47 2026 +0000
tree: b8082a3da289c9c38d9a2d1bf814f9a4cb4b9215
parent: 6778cc8342791e48cc5b8aa6243ce16e2bed582b [diff]

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`.

src/Init/Data/List/Basic.lean[diff]

1 file changed

tree: b8082a3da289c9c38d9a2d1bf814f9a4cb4b9215

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.