commit: 2d91e9b14cd281d2c2938ca427c9dba60d3d82d3

[log]
author: Kim Morrison <kim@tqft.net>

Tue Nov 25 02:40:58 2025 +0100
committer: Kim Morrison <kim@tqft.net>

Tue Nov 25 02:50:56 2025 +0100
tree: 4bccb628e92cbf73188fc7121e1e45d9c03dcdcb
parent: f2e191d0afbb5adcc6f12e1779c8b141fc9af996 [diff]

feat: implement `grind_annotated` command

- Add syntax declaration in Init/Grind/Annotated.lean
- Add elaborator with YYYY-MM-DD date validation in Lean/Elab/Tactic/Grind/Annotated.lean
- Add SimplePersistentEnvExtension to track grind-annotated modules
- Add filterGrindAnnotated wrapper for Selector
- Apply filter to sineQuaNonSelector in default library suggestions
- Set caller field to "grind" when grind tactic calls LibrarySuggestions

10 files changed

tree: 4bccb628e92cbf73188fc7121e1e45d9c03dcdcb

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.