commit: 8e4c38968f3ed8c25155bd2de591cab833994324

[log]
author: Violeta Hernández <vi.hdz.p@gmail.com>

Sun Apr 06 19:34:40 2025 -0600
committer: GitHub <noreply@github.com>

Mon Apr 07 01:34:40 2025 +0000
tree: 61b4a608b7c08576502842ac5dc162b0080c51a4
parent: c97092bef8428570d8ab737f03f63426bff075af [diff]

feat: two new lemmas on `List.head` / `List.getLast` (#7108)

This PR proves `List.head_of_mem_head?` and the analogous
`List.getLast_of_mem_getLast?`.

These are similar to the existing `List.head_eq_iff_head?_eq_some` and
`List.getLast_eq_iff_getLast?_eq_some`, with the added convenience that
the proof term needs not be given.

---------

Co-authored-by: Kim Morrison <kim@tqft.net>

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

1 file changed

tree: 61b4a608b7c08576502842ac5dc162b0080c51a4

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean (documentation source: doc/make/index.md).