Skip to content

[Lean] Grind Linter #1960

New issue
New issue
Open
Open
[Lean] Grind Linter#1960
Labels
leanRelated to the Lean backend or libraryproof-libIssues related the backend-specific definitions (in the proof-lib folder)
@abentkamp

Description

@abentkamp
abentkamp
opened on Feb 18, 2026

We should use grind_lint to check our grind annotations. Here is how this was done in mathlib:
https://github.com/leanprover-community/mathlib4/pull/31866/changes

Metadata

Metadata

Assignees

No one assigned

    Labels

    leanRelated to the Lean backend or libraryproof-libIssues related the backend-specific definitions (in the proof-lib folder)

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions