commit: f4c9934171a22d376fb7c318ce2dcf80ab0eaf0e

[log]
author: Kim Morrison <scott.morrison@gmail.com>

Thu Jan 16 17:33:54 2025 +1100
committer: GitHub <noreply@github.com>

Thu Jan 16 06:33:54 2025 +0000
tree: 847e187d8ec18a9fab2be6afb92f593d5c187938
parent: 80ddbf45eb92794b1df2cb625e9432753d41601b [diff]

feat: Vector.getElem_flatMap (#6661)

This PR adds array indexing lemmas for `Vector.flatMap`. (These were not
available for `List` and `Array` due to variable lengths.)

2 files changed

tree: 847e187d8ec18a9fab2be6afb92f593d5c187938

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