commit: 06d05d1f4698a48ba5ca6ad7f753c3674c5f8cc7

[log]
author: Leonardo de Moura <leomoura@amazon.com>

Thu Aug 14 15:47:42 2025 -0700
committer: GitHub <noreply@github.com>

Thu Aug 14 22:47:42 2025 +0000
tree: 9e717403bf07c551287b435cfb9c49fe9786de7b
parent: fe7e0859d58d7c28314526a97f6a4e467895210a [diff]

feat: missing `grind` annotations (#9921)

This PR marks `List.drop_length` and `List.take_length` with `[grind
=]`.

2 files changed

tree: 9e717403bf07c551287b435cfb9c49fe9786de7b

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.