Repository Issue Activity (beta)

#5598 RFC: `unless` doesn't support hypothesis like e.g. `if h: ...`

#13050 bad interplay between grind/sym interactive modes and grind order

#14275 Goal pretty-printing doesn't respect `pp.instantiateMVars`

#14264 `lambdaMetaTelescope` doesn't preserve binder names

#13996 lake: module archives are not content-stable, preventing cache deduplication and reuse

#14152 RFC: `lake cache get` read chain from multiple services

#14154 RFC: Configurable / default `lake cache` scopes

#14246 Std.Async.Selectable.one uses system entropy in hot path

#14233 Verso docstring on `coinductive` gives error "Couldn't interpret binder"

#14218 open in term elaborator does not update InfoTree context

#13753 Circular wording in `#eval` docstring

#13007 docstrings missmarked as comments

#12813 Verso docstring on `where` declaration with match causes error

#14221 RFC: Use Zig as the primary build orchestration layer for Lean4

#14151 RFC: SHA-isolated `lake cache get` via configurable revision discovery

#14208 Conflicting `simp` lemmas `List.push_append_toArray` and `Array.append_singleton`

#11746 `exact? +grind` uses the declaration it's in recursively

#7525 Infinite loop in `simp`: `ite_congr not modified`

#2920 `linter.unusedVariables` false positive when used in `decreasing_by`

#13705 `exact?` and `grind` block on prior async theorem bodies

#14090 `Selectable.combine` can hang and panic

#13113 set_next and get_next truncate pointers unsafely on some x86 and ARM configurations

#13685 IR eta-expansion through trivial structure

#13572 `lia` fails with "(kernel) application type mismatch"

#13592 simp? returns unuseful lemmas