Repository Issue Activity (beta)

#13818 RFC: distinguish parser errors and elaboration errors

#13861 lake lint: support excluding modules from linting

#13638 RFC: Redesign of Lean FS API

#8930 error: Error: tag for constructor 'ast.ZIMOP_MOP_RR' is too big, this is a limitation of the current runtime

#8942 RFC: Remove Redundant Deprecation Warnings

#13673 RFC: hover for `fun_induction`

#11631 `grind` fails where `subst; grind` succeeds

#13581 `set_option diagnostics true` fails with 'Unknown constant' on private `_sparseCasesOn_*` / `match_*` helpers in `module` mode

#13355 LCNF ReduceArity should also work for non-fix unused arguments.

#13364 Failure to generate equality theorem for matcher

#13408 Kernel error for `inferInstanceAs` with let declarations

#13411 Hover shows resolved type but error shows unresolved metavariable

#13424 `rw` inserts rewritten hypothesis that forward-references fvar

#13439 Recursive `unsafe opaque` declarations are not opaque

#13444 Termination checker error appears on the wrong invocation

#13465 Strict positivity constraints for inductive behave differently on a type alias

#13469 Slow HTTP Server Performance

#13473 The inferred level for structures doesn't always work

#13508 Wrong type in hover on nested `sepBy` antiquotation

#13509 Cannot derive functional induction principle for a recursive function: 'still depends on' named pattern matches

#13561 `BitVec.ofBoolListLE` stack overflow for large lists

#13570 `set_option maxErrors` does not work

#13571 Inconsistent behavior in typeclass resolution (local vs top-level instance)

#13632 LCNF simplifier scales super-linearly

#13515 Please, provide a way to ensure that given function is panic-free. For example, by making panic opaque