8000 feat: improve error message when passing local hypotheses to `grind` by marcusrossel · Pull Request #8891 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

feat: improve error message when passing local hypotheses to grind#8891

Draft
marcusrossel wants to merge 1 commit intoleanprover:masterfrom
marcusrossel:grind-locals
Draft

feat: improve error message when passing local hypotheses to `grind`#8891
marcusrossel wants to merge 1 commit intoleanprover:masterfrom
marcusrossel:grind-locals

Commits

Commits on Jun 20, 2025
0