GitHub · Where software is built

Labels Milestones New issue

Syntax match strange error

#11951

· PatrickMassot opened

on Jan 9, 2026

'import all' sometimes still requires @[expose] when using grind

#11948

· cmlsharp opened

on Jan 9, 2026

<code>match</code> generalization failure

changelog-language

#11942

· sgraf812 opened

on Jan 8, 2026

leanchecker: mention declaration name in error

#11937

· nomeata opened

on Jan 8, 2026

Class abbreviations can't be protected

#11931

· hatzka-nezumi opened

on Jan 8, 2026

<code>unknown free variable</code> for recursive <code>grind</code> terms

#11930

· chenson2018 opened

on Jan 8, 2026

linter.unusedSectionVars: does not detect variable uses in where clauses

#11917

· kim-em opened

on Jan 6, 2026

panic in grind

#11910

· kim-em opened

on Jan 6, 2026

grind: cannot teach grind that (¬(x = none)) -> (∃ y, x = some y)

#11897

· safinaskar opened

on Jan 5, 2026

"This pattern contains metavariables" when using structure constructor and omitting a proof parameter

#11885

· kmill opened

on Jan 3, 2026

<code>conv in</code> can unexpectedly fail with <code>unknown metavariable</code> error

#11877

· vlad902 opened

on Jan 2, 2026

grind/grobner doesn't finish a proof for a medium-sized problem within reasonable limit

#11861

· wwylele opened

on Jan 1, 2026