Search results

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

bugSomething isn't workingSomething isn't working

Status: Open.

#13509 In leanprover/lean4;

· raoxiaojia opened on Apr 22, 2026

Wrong type in hover on nested sepBy antiquotation

bugSomething isn't workingSomething isn't working

Status: Open.

#13508 In leanprover/lean4;

· mhuisi opened on Apr 22, 2026

lake update and lake exe cache get first clone full mathlib repo instead of shallow clone at a given rev

bugSomething isn't workingSomething isn't working

Status: Open.

#13504 In leanprover/lean4;

· vadimkantorov opened on Apr 22, 2026

lake exe myprojectname on MacOS leads to error "Argument list too long" because clang command has all mathlib object files full paths

bugSomething isn't workingSomething isn't working

Status: Open.

#13503 In leanprover/lean4;

· vadimkantorov opened on Apr 22, 2026

"#printaxioms" is wrongly accepted by parser

bugSomething isn't workingSomething isn't working

Status: Open.

#13496 In leanprover/lean4;

· safinaskar opened on Apr 21, 2026

The inferred level for structures doesn't always work

bugSomething isn't workingSomething isn't working

Status: Open.

#13473 In leanprover/lean4;

· Rob23oba opened on Apr 19, 2026

Slow HTTP Server Performance

enhancementNew feature or requestNew feature or request

nice to haveCool feature that would be really nice to haveCool feature that would be really nice to have

Status: Open.

Feature

#13469 In leanprover/lean4;

· algebraic-dev opened on Apr 18, 2026

Strict positivity constraints for inductive behave differently on a type alias

bugSomething isn't workingSomething isn't working

Status: Open.

#13465 In leanprover/lean4;

· tribbloid opened on Apr 18, 2026

IO.Process.output duplicates buffered file writes when exec fails

Status: Open.

#13463 In leanprover/lean4;

· kim-em opened on Apr 18, 2026

Incremental build cache can cause incorrect test results

bugSomething isn't workingSomething isn't working

LakeLake related issueLake related issue

Status: Open.

#13449 In leanprover/lean4;

· robin-aws opened on Apr 17, 2026

Termination checker error appears on the wrong invocation

bugSomething isn't workingSomething isn't working

Status: Open.

#13444 In leanprover/lean4;

· TwoFX opened on Apr 17, 2026

Recursive unsafe opaque declarations are not opaque

bugSomething isn't workingSomething isn't working

Status: Open.

#13439 In leanprover/lean4;

· Rob23oba opened on Apr 17, 2026