commit: c9708e7bd7cf47106e2fc063d3c586c8f333e54d

[log]
author: Chris Henson <46805207+chenson2018@users.noreply.github.com>

Sun Mar 22 12:54:33 2026 -0400
committer: GitHub <noreply@github.com>

Sun Mar 22 16:54:33 2026 +0000
tree: 9b222629e0ec0e8f77a8f95239effa75cf394f0f
parent: 8f6411ad576cc0bec3e9a891c60df223da300a71 [diff]

doc: update docstring of `Lean.Parser.Tactic.Grind.first` (#12998)

This PR updates the docstring for `Lean.Parser.Tactic.Grind.first`,
which changed syntax in #10828.

src/Init/Grind/Interactive.lean[diff]

1 file changed

tree: 9b222629e0ec0e8f77a8f95239effa75cf394f0f

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.