commit: 48be424eaa2ae06972e9cfec4d355906b532204d

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

Thu Dec 12 15:48:34 2024 +1100
committer: GitHub <noreply@github.com>

Thu Dec 12 04:48:34 2024 +0000
tree: 640ba0792e2085c43a1372d54bdc17242262e8d6
parent: 58f8e215022173931b4bb8d0635aca9faf8bcce5 [diff]

feat: lemmas about Vector.any/all/set (#6369)

This PR adds lemmas about `Vector.set`, `anyM`, `any`, `allM`, and
`all`.

With these additions, `Vector` is now as in-sync with the `List` API as
`Array` is, and in future I'll be updating both simultaneously.

3 files changed

tree: 640ba0792e2085c43a1372d54bdc17242262e8d6

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