Pulse · leanprover/lean4

June 19, 2025 – June 26, 2025

291 Unresolved conversations

Sometimes conversations happen on old items that aren’t yet closed. Here is a list of all the Issues and Pull Requests with unresolved conversations.

fix: `match` discriminant congruence in `simp`
#8884 commented on Jun 26, 2025 • 20 new comments
feat: add `lean_setup_libuv` for initializing required LIBUV components
#8636 commented on Jun 26, 2025 • 8 new comments
feat: add DNS resolution functions to the standard library
#8072 commented on Jun 26, 2025 • 6 new comments
feat: add system information functions to the standard library
#8109 commented on Jun 26, 2025 • 3 new comments
feat: add fast circuit for unsigned multiplication overflow detection `fastUmulOverflow_eq` and definitions
#7858 commented on Jun 26, 2025 • 2 new comments
10000
feat: show declaration keywords in hovers
#7232 commented on Jun 26, 2025 • 0 new comments
feat: abstract proofs in all declaration types
#7181 commented on Jun 26, 2025 • 0 new comments
feat: make `rw` diagnose instance argument mismatch (experimental)
#7172 commented on Jun 26, 2025 • 0 new comments
feat: add RPINF
#7008 commented on Jun 26, 2025 • 0 new comments
feat: add `BitVec.(getElem, getLsbD, getMsbD, msb)_smod` theorems
#6986 commented on Jun 26, 2025 • 0 new comments
fix: FileSystem.normalize
#6983 commented on Jun 26, 2025 • 0 new comments
doc: standard library design principles
#6974 commented on Jun 26, 2025 • 0 new comments
fix: set `iota := true` in `simpGlobalConfig`
#6909 commented on Jun 26, 2025 • 0 new comments
feat: lake: async imports
#6894 commented on Jun 26, 2025 • 0 new comments
feat: allow simp priority explanations
#6811 commented on Jun 26, 2025 • 0 new comments
feat: Confluent simp-set for left shift by BitVec.twoPow
#6782 commented on Jun 26, 2025 • 0 new comments
feat: bitblasting support for `BitVec.carry`
#6766 commented on Jun 26, 2025 • 0 new comments
feat: allow separate handlers for literals and interpolations in `expandInterpolatedStr`
#6763 commented on Jun 26, 2025 • 0 new comments
feat: add conversion-mode `clear` tactic
#6732 commented on Jun 26, 2025 • 0 new comments
fix: avoid nonexistent `noConfusion`s in `injection`, `contradiction`
#6731 commented on Jun 26, 2025 • 0 new comments
feat: set priority in monadic class instances
#6725 commented on Jun 26, 2025 • 0 new comments
feat: `Nat.decidableBallLT` handles large numbers
#6651 commented on Jun 26, 2025 • 0 new comments
feat: Constructions for splitting and merging vectors of bitvectors
#7754 commented on Jun 26, 2025 • 0 new comments
fix: finalize libuv
#7752 commented on Jun 26, 2025 • 0 new comments
perf: add a bitblasting cache for bv_decide's boolean substructure
#7707 commented on Jun 26, 2025 • 0 new comments
feat: allow a general `evalTac` at `evalSepTactics`
#7702 commented on Jun 26, 2025 • 0 new comments
feat: async elaboration of theorem types
#7597 commented on Jun 26, 2025 • 0 new comments
perf: avoid `isDefEq` in constructing `simp` proof term
#7585 commented on Jun 26, 2025 • 0 new comments
fix: use pi_congr instead of forall_congr; deprecate the latter
#7577 commented on Jun 26, 2025 • 0 new comments
feat: kernel: lazy_delta_reduction: try to reduce_nat
#7545 commented on Jun 26, 2025 • 0 new comments
feat: `run_macro` & `run_cmd_macro`
#7524 commented on Jun 26, 2025 • 0 new comments
chore: run tests with `LEAN_ABORT_ON_PANIC`
#7470 commented on Jun 26, 2025 • 0 new comments
feat: add min and max to seval
#7464 commented on Jun 26, 2025 • 0 new comments
feat: Nat.dfold
#7450 commented on Jun 26, 2025 • 0 new comments
feat: lemmas about filterM
#7423 commented on Jun 26, 2025 • 0 new comments
feat: (experiment) have synth order defer "mixin" instances
#7313 commented on Jun 26, 2025 • 0 new comments
feat: let synth order checker detect generalized projections
#7310 commented on Jun 26, 2025 • 0 new comments
fix: `IO.Process.spawn` on windows
#8612 commented on Jun 26, 2025 • 0 new comments
fix: inline `Nat.cast`
#7283 commented on Jun 26, 2025 • 0 new comments
feat: define `Squash` as a `Quotient`
#6642 commented on Jun 26, 2025 • 0 new comments
feat: allow limiting the number of binders in delabConstWithSignature
#6092 commented on Jun 26, 2025 • 0 new comments
doc: `MkBinding.abstractRange` doesn't do anything with types of free variables
#6089 commented on Jun 26, 2025 • 0 new comments
chore: `collectForwardDeps` returns only free variables, not metavars
#6088 commented on Jun 26, 2025 • 0 new comments
chore: add error instructions for lake build failure troubleshooting
#6028 commented on Jun 26, 2025 • 0 new comments
feat: `change_matching ... with` tactic
#6018 commented on Jun 26, 2025 • 0 new comments
refactor: use `Json.null` to represent `Name.anonymous`
#5980 commented on Jun 26, 2025 • 0 new comments
feat: simp -underLambda
#5977 commented on Jun 26, 2025 • 0 new comments
feat: `lift_match` simproc and conv tactic
#5923 commented on Jun 26, 2025 • 0 new comments
feat: structural recursion: support more nested matches
#5849 commented on Jun 26, 2025 • 0 new comments
feat: stronger proof strategy for `partial` inhabitation
#5847 commented on Jun 26, 2025 • 0 new comments
feat: rsimp_decide etc
#5839 commented on Jun 26, 2025 • 0 new comments
fix: make prefix `!` require that there be no whitespace after it
#5826 commented on Jun 26, 2025 • 0 new comments
fix: reduce precedence of prefix `!` to 'lead'
#5824 commented on Jun 26, 2025 • 0 new comments
feat: Pass `argv[0]` to `main`
#5820 commented on Jun 26, 2025 • 0 new comments
feat: simp local confluence testing
#5717 commented on Jun 26, 2025 • 0 new comments
refactor: construct `.eq_def` before `.eq_n`
#5669 commented on Jun 26, 2025 • 0 new comments
chore: add example where omega never terminates / runs out of heartbeats
#5662 commented on Jun 26, 2025 • 0 new comments
perf: `infer_app` with `infer_only := false` (WIP)
#2781 commented on Jun 26, 2025 • 0 new comments
feat: allow more Unicode characters in identifiers
#6579 commented on Jun 26, 2025 • 0 new comments
fix: reduce `Eq.rec` when mvars are present
#6577 commented on Jun 26, 2025 • 0 new comments
fix: respect explicitly inaccessible pattern variables
#6558 commented on Jun 26, 2025 • 0 new comments
docs: msys2: leaving a helpful note
#6552 commented on Jun 26, 2025 • 0 new comments
fix: don't treat non-atomic idents as pattern variables
#6551 commented on Jun 26, 2025 • 0 new comments
chore: add regression test for issue 5925
#6511 commented on Jun 26, 2025 • 0 new comments
fix: make sure `#guard_*` uses syntactic equality
#6483 commented on Jun 26, 2025 • 0 new comments
perf: tune Array.push runtime code
#6471 commented on Jun 26, 2025 • 0 new comments
feat: change `pp.natLit` to be enabled by default
#6439 commented on Jun 26, 2025 • 0 new comments
fix: make sure `isDefEqSingleton` rule checks types
#6421 commented on Jun 26, 2025 • 0 new comments
chore: permit Lake failures in PR release CI
#6403 commented on Jun 26, 2025 • 0 new comments
feat: runtime primitives for mpz objects
#6395 commented on Jun 26, 2025 • 0 new comments
feat: improved `export` command, namespace aliases
#6393 commented on Jun 26, 2025 • 0 new comments
feat: tweak delta expansion heuristics
#6335 commented on Jun 26, 2025 • 0 new comments
feat: warnings when declarations and `export` aliases conflict
#6269 commented on Jun 26, 2025 • 0 new comments
feat: `dotParam` widget to control dot notation
#6267 commented on Jun 26, 2025 • 0 new comments
chore: upstream `nolint` attribute
#6215 commented on Jun 26, 2025 • 0 new comments
feat: attribute delaborators
#6115 commented on Jun 26, 2025 • 0 new comments
fix: lake: test flakiness
#8580 commented on Jun 26, 2025 • 0 new comments
feat: add word-level hint suggestion diffs
#8574 commented on Jun 26, 2025 • 0 new comments
fix: add names to type signature of MonadWithReader.withReader
#8563 commented on Jun 26, 2025 • 0 new comments
doc: fix "lean-manual" URL scheme in style guide example
#8558 commented on Jun 26, 2025 • 0 new comments
doc: capitalize some theorem names according to style guide
#8557 commented on Jun 26, 2025 • 0 new comments
doc: replace straight single quotes with typographical ones in style guide
#8556 commented on Jun 26, 2025 • 0 new comments
doc: add "lean" language tag to all code blocks in style guide
#8555 commented on Jun 26, 2025 • 0 new comments
doc: fix inline code formatting in style guide
#8553 commented on Jun 26, 2025 • 0 new comments
doc: include an example for "split infinitives" in style guide
#8551 commented on Jun 26, 2025 • 0 new comments
feat: dot auto-completion for identifiers outside of terms
#8525 commented on Jun 26, 2025 • 0 new comments
feat: `revert e` for arbitrary terms
#8522 commented on Jun 26, 2025 • 0 new comments
chore: add failing grind tests
#8518 commented on Jun 26, 2025 • 0 new comments
fix: incorrect arrow orientations in grind syntax
#8517 commented on Jun 26, 2025 • 0 new comments
feat: `congr_simp` as realizable constant
#8474 commented on Jun 26, 2025 • 0 new comments
feat: Optionally use sccache instead of ccache
#8444 commented on Jun 26, 2025 • 0 new comments
Draft: Do not duplicate old MVars in `apply`
#8441 commented on Jun 26, 2025 • 0 new comments
test: FunInd vs. module system
#8151 commented on Jun 26, 2025 • 0 new comments
perf: better isDefEq cache in the presence of metavariables
#8883 commented on Jun 26, 2025 • 0 new comments
feat: links libidn2
#8871 commented on Jun 26, 2025 • 0 new comments
feat: complete level def eq
#8867 commented on Jun 26, 2025 • 0 new comments
fix: walk through types of axioms in `collectAxioms`
#8842 commented on Jun 26, 2025 • 0 new comments
draft: range migration test run
#8841 commented on Jun 26, 2025 • 0 new comments
feat: allow access to private names through `import all`
#8828 commented on Jun 26, 2025 • 0 new comments
fix: opacify functions using {Expr,Level}.data
#8821 commented on Jun 26, 2025 • 0 new comments
feat: `debug.elabCheck` option to enable elaborator type checking
#8819 commented on Jun 26, 2025 • 0 new comments
doc: fix typo in docstring for `fieldIdxKind`
#8814 commented on Jun 26, 2025 • 0 new comments
fix: lake: `lean --setup` integration performance
#8787 commented on Jun 26, 2025 • 0 new comments
doc: fix broken "quickstart" and "supported editors" link
#8785 commented on Jun 26, 2025 • 0 new comments
feat: better universe normalization
#8769 commented on Jun 26, 2025 • 0 new comments
fix: revert state on compilation failure (new compiler)
#8691 commented on Jun 26, 2025 • 0 new comments
fix: make `kabstract` unify types before unifying terms
#8667 commented on Jun 26, 2025 • 0 new comments
perf: do not import non-template IR for codegen
#8666 commented on Jun 26, 2025 • 0 new comments
perf: restrict imported IR
#8664 commented on Jun 26, 2025 • 0 new comments
feat: `warn.sorry` option
#8662 commented on Jun 26, 2025 • 0 new comments
feat: Add `getElem_unzip` lemmas
#8644 commented on Jun 26, 2025 • 0 new comments
experiment: allow postponing defeq failure if there are mvars
#8074 commented on Jun 26, 2025 • 0 new comments
experiment: allow mvar applications in elaborator
#8073 commented on Jun 26, 2025 • 0 new comments
feat: `BaseIO.joinTask`
#8070 commented on Jun 26, 2025 • 0 new comments
feat: in app elaborator, beta reduce when substituting arguments
#7991 commented on Jun 26, 2025 • 0 new comments
feat: deprecated options
#7969 commented on Jun 26, 2025 • 0 new comments
feat: infoAsError
#7968 commented on Jun 26, 2025 • 0 new comments
feat: dedicated fix operator for well-founded recursion on Nat
#7965 commented on Jun 26, 2025 • 0 new comments
feat: hovers when `pp.oneLine` is true
#7954 commented on Jun 26, 2025 • 0 new comments
fix: synthesize instances for induction/cases targets
#7944 commented on Jun 26, 2025 • 0 new comments
perf: update to cadical 2.2.0
#7942 commented on Jun 26, 2025 • 0 new comments
feat: always show `nat_lit`, simpler hovers for `OfNat` literals
#7896 commented on Jun 26, 2025 • 0 new comments
feat: (experiment) use low priority for parent instances
#7894 commented on Jun 26, 2025 • 0 new comments
feat: basic premise selection algorithm based on MePo
#7844 commented on Jun 26, 2025 • 0 new comments
feat: Add sorried lemmas about unions of `Raw₀`
#7823 commented on Jun 26, 2025 • 0 new comments
perf: avoid duplicate work in `simp` when there are bound variables
#7804 commented on Jun 26, 2025 • 0 new comments
chore: update to mimalloc 3.0.3 beta
#7786 commented on Jun 26, 2025 • 0 new comments
chore: add docstring to `Simp.Methods.discharge?`
#7779 commented on Jun 26, 2025 • 0 new comments
feat: let `simp` simplify numerals
#8433 commented on Jun 26, 2025 • 0 new comments
feat: Add `getElem_swapIfInBounds*` lemmas and deprecate `getElem_swap'`
#8406 commented on Jun 26, 2025 • 0 new comments
chore: turn some crashes into errors
#8402 commented on Jun 26, 2025 • 0 new comments
feat: unexpand `Vector.mk #[...] _` to `#v[...]`
#8391 commented on Jun 26, 2025 • 0 new comments
feat: add `msb_neg_of_msb_false`, `msb_neg_of_msb_true`, `msb_neg_umod_neg_of_msb_true_of_msb_true`, `msg_neg_neg_mod_neg`
#8376 commented on Jun 26, 2025 • 0 new comments
feat: use Meta.letToHave
#8373 commented on Jun 26, 2025 • 0 new comments
doc: also mention the full syntax for the deprecated attribute
#8339 commented on Jun 26, 2025 • 0 new comments
chore: `Decidable` as subtype of `Bool` using the new compiler
#8309 commented on Jun 26, 2025 • 0 new comments
Experiments with metavar error reporting
#8307 commented on Jun 26, 2025 • 0 new comments
perf: make `Lean.Meta.Check` messages lazy
#8283 commented on Jun 26, 2025 • 0 new comments
feat: improve infer binder type failure message and range
#8263 commented on Jun 26, 2025 • 0 new comments
fix: nested try-catch parsing
#8252 commented on Jun 26, 2025 • 0 new comments
feat: guard against synthetic sorry misuse
#8230 commented on Jun 26, 2025 • 0 new comments
chore: link against system glibc
#8229 commented on Jun 26, 2025 • 0 new comments
fix: aborting elaboration should not lead to empty `#print axioms`
#8214 commented on Jun 26, 2025 • 0 new comments
feat: characterize when T-division equals zero
#8204 commented on Jun 26, 2025 • 0 new comments
feat: expand byte array api
#8165 commented on Jun 26, 2025 • 0 new comments
fix: `isDefEq` argument order in `simp` for `binderNameHint`
#8155 commented on Jun 26, 2025 • 0 new comments
fix: bug in gen_injective_theorems%
#2355 commented on Jun 26, 2025 • 0 new comments
Sort messages by position when printing
#2335 commented on Jun 26, 2025 • 0 new comments
Make token parser customizable
#2293 commented on Jun 26, 2025 • 0 new comments
feat: `opaque_repr` attribute to suppress "trivial structure" opt
#2292 commented on Jun 26, 2025 • 0 new comments
fix: respect type reducibility when generating injectivity lemmas
#2276 commented on Jun 26, 2025 • 0 new comments
feat: `eta_reduce_fun%` in cdot parser, v2
#2267 commented on Jun 26, 2025 • 0 new comments
feat: `eta_reduce_fun%` in cdot parser
#2263 commented on Jun 26, 2025 • 0 new comments
fix: resolve `_root_` in `macro`, `syntax`, `elab`
#2239 commented on Jun 26, 2025 • 0 new comments
chore: use binderIdent consistently in grammar
#2105 commented on Jun 26, 2025 • 0 new comments
fix: #include <mutex> in mutex.cpp
#2094 commented on Jun 26, 2025 • 0 new comments
fix: LLVM backend: detect size_t from target triple
#2090 commented on Jun 26, 2025 • 0 new comments
Use `Bool.asProp` for coercions
#2060 commented on Jun 26, 2025 • 0 new comments
Make `Decidable` a subtype of `Bool`
#2038 commented on Jun 26, 2025 • 0 new comments
chore: CI: enable emulated tests on Linux aarch64
#1913 commented on Jun 26, 2025 • 0 new comments
feat: `show` tactic (full version)
#1749 commented on Jun 26, 2025 • 0 new comments
[WIP] feat: Suggest tactic
#1665 commented on Jun 26, 2025 • 0 new comments
`Nat.toDigits` with base `1`
#8686 commented on Jun 26, 2025 • 0 new comments
Can't compile for loop with two mut vars in an if branch
#7874 commented on Jun 25, 2025 • 0 new comments
feat: change `(d)simp`'s default `zeta` value to `false`
#2779 commented on Jun 26, 2025 • 0 new comments
test: remove optimization
#2748 commented on Jun 26, 2025 • 0 new comments
perf: [kernel] switch defeq order in infer_app
#2704 commented on Jun 26, 2025 • 0 new comments
fix: bug in elab TC for projections
#2700 commented on Jun 26, 2025 • 0 new comments
feat: remove configuration olean on `lake clean`
#2699 commented on Jun 26, 2025 • 0 new comments
feat: mark `rfl` proofs of `Iff` for use by `dsimp`
#2679 commented on Jun 26, 2025 • 0 new comments
fix: bug in do expansion
#2676 commented on Jun 26, 2025 • 0 new comments
chore: simplify is_rec / is_reflexive
#2674 commented on Jun 26, 2025 • 0 new comments
chore: make IO.RealWorld opaque
#2656 commented on Jun 26, 2025 • 0 new comments
refactor: simplify excluded middle proof
#2625 commented on Jun 26, 2025 • 0 new comments
feat: mark predefinitions that failed to compile as noncomputable
#2610 commented on Jun 26, 2025 • 0 new comments
chore: indentation before `|`
#2581 commented on Jun 26, 2025 • 0 new comments
feat: lake: add `lake dump-config` command
#2542 commented on Jun 26, 2025 • 0 new comments
feat: exprDependsOn follows delayed assignments
#2484 commented on Jun 26, 2025 • 0 new comments
doc: use {b_}obj_{arg,res} consistently in lean.h
#2466 commented on Jun 26, 2025 • 0 new comments
feat: FFI thread initialization
#2464 commented on Jun 26, 2025 • 0 new comments
fix: deprecation span should only cover the ident
#2459 commented on Jun 26, 2025 • 0 new comments
feat: include `ppLine` in `many(1)Indent`
#2453 commented on Jun 26, 2025 • 0 new comments
SIGSEGV in elaboration
#4703 commented on Jun 20, 2025 • 0 new comments
unknown free variable since v4.8.0
#4418 commented on Jun 20, 2025 • 0 new comments
bug: projection on `unsafeCast` leads to "unknown free variable: _neutral" error/segfault
#8407 commented on Jun 20, 2025 • 0 new comments
Control run-time execution of pure functions
#8591 commented on Jun 20, 2025 • 0 new comments
unknown free variable: _kernel_fresh.1210
#4548 commented on Jun 20, 2025 • 0 new comments
using Option.attach can crash lean
#6957 commented on Jun 20, 2025 • 0 new comments
"compiler IR check failed" error when trying to create `ToString` instance
#2602 commented on Jun 20, 2025 • 0 new comments
Fields having inductive types with trivial structure are always stored boxed
#2589 commented on Jun 20, 2025 • 0 new comments
Do notation inhibits tail call optimization
#444 commented on Jun 20, 2025 • 0 new comments
Code generator support for recursors
#2049 commented on Jun 20, 2025 • 0 new comments
Compiler error with subtypes of erased types
#2104 commented on Jun 20, 2025 • 0 new comments
"unknown free variable" kernel error with complex `do` block
#1415 commented on Jun 20, 2025 • 0 new comments
Invalid projection on field of a dependent cast in a dependent structure constructor
#1370 commented on Jun 20, 2025 • 0 new comments
Revise closed term extraction
#467 commented on Jun 20, 2025 • 0 new comments
Linear code leads to non-linear IR
#6058 commented on Jun 20, 2025 • 0 new comments
If-then-else breaks apparent linearity
#2218 commented on Jun 20, 2025 • 0 new comments
RFC: linters should be able to use try this
#4363 commented on Jun 20, 2025 • 0 new comments
Error "(kernel) application type mismatch" in theorem on inductive type
#8839 commented on Jun 20, 2025 • 0 new comments
Universe level normalization has associativity of `max` backwards from parsing associativity
#5695 commented on Jun 25, 2025 • 0 new comments
Turning `abbrev` into `def` defeats type inference
#8766 commented on Jun 25, 2025 • 0 new comments
Interleaved expected output in leantest_csimpAttr.lean?
#1451 commented on Jun 21, 2025 • 0 new comments
Some functions using `List.foldr` are specialized for common argument types before the tail-recursive `foldr` is available
#7750 commented on Jun 21, 2025 • 0 new comments
Inferred value for implicit argument leads to suboptimal IR
#4157 commented on Jun 21, 2025 • 0 new comments
INTERNAL PANIC: unreachable code has been reached
#5774 commented on Jun 21, 2025 • 0 new comments
Linearisation failure in `Array.mapMUnsafe`
#4699 commented on Jun 21, 2025 • 0 new comments
Bad performance on iterated HOrElse
#2227 commented on Jun 20, 2025 • 0 new comments
Slow code generation for an instance declaration
#6328 commented on Jun 20, 2025 • 0 new comments
Mutual recursion and `@[specialize]` lead to `(kernel) deep recursion detected`
#4716 commented on Jun 20, 2025 • 0 new comments
Closed-term extraction creates out-of-bound array accesses
#1965 commented on Jun 20, 2025 • 0 new comments
Add a safe wrapper around `ptrEq`
#1502 commented on Jun 20, 2025 • 0 new comments
FFI generates boxed accessor for a trivial structure containing a UInt64 inside nontrivial structure
#427 10000 8 commented on Jun 20, 2025 • 0 new comments
Decide on memory representation of opaque type definitions
#1536 commented on Jun 20, 2025 • 0 new comments
compiler produces `(kernel) function expected`
#1774 commented on Jun 20, 2025 • 0 new comments
kernel invalid projection in old code generator
#3761 commented on Jun 20, 2025 • 0 new comments
Importing a `Lean` module inflates binary size
#5274 commented on Jun 20, 2025 • 0 new comments
Closed term extraction for large list literals produces large call stacks
#6047 commented on Jun 20, 2025 • 0 new comments
feat: Strict Ackermannization (bv_ac_eager) tactic for QF_UFBV
#5657 commented on Jun 26, 2025 • 0 new comments
perf: partially inline `lean_dec_ref_cold`
#5017 commented on Jun 26, 2025 • 0 new comments
perf: destructive update at `expr_eq_fn`
#4994 commented on Jun 26, 2025 • 0 new comments
perf: inline `lean_inc_ref_cold`
#4978 commented on Jun 26, 2025 • 0 new comments
feat: make loose docstrings into elaboration errors rather than parse errors
#4975 commented on Jun 26, 2025 • 0 new comments
chore: constructorNameAsVariable linter respects linter.all
#4966 commented on Jun 26, 2025 • 0 new comments
perf: cache binop elaborator
#4938 commented on Jun 26, 2025 • 0 new comments
feat: warnings for commands that do not have desired effects in particular contexts
#4892 commented on Jun 26, 2025 • 0 new comments
fix: improve proof search in IndPredBelow
#4840 commented on Jun 26, 2025 • 0 new comments
feat: make `structure` command encode (some) optional parameters in the constructor
#4825 commented on Jun 26, 2025 • 0 new comments
chore: refactor String definitions
#4641 commented on Jun 26, 2025 • 0 new comments
feat: consistent elaboration of tactic `have ... by`
#4626 commented on Jun 26, 2025 • 0 new comments
feat: @[simp] Nat.add_assoc'
#4557 commented on Jun 26, 2025 • 0 new comments
feat: suggest fixes for potentially misspelled identifiers
#4552 commented on Jun 26, 2025 • 0 new comments
chore: use ' instead of brackets for quotes
#4464 commented on Jun 26, 2025 • 0 new comments
Moving String theorems from Basic to Lemmas
#4393 commented on Jun 26, 2025 • 0 new comments
perf: cache intermediate type class results and non-results
#4272 commented on Jun 26, 2025 • 0 new comments
feat: fat static libraries with all transitive dependencies
#4271 commented on Jun 26, 2025 • 0 new comments
chore: minimization of variable-induced slowdown
#4253 commented on Jun 26, 2025 • 0 new comments
chore: add LNSym omega benchmarks with large problems that take multiple seconds to solve
#5622 commented on Jun 26, 2025 • 0 new comments
fix: bug in apply? when using intro
#5589 commented on Jun 26, 2025 • 0 new comments
chore: adjust DecidableRel instance for leOfOrd
#5537 commented on Jun 26, 2025 • 0 new comments
chore: deprecate variants other than `inductive ... where`
#5533 commented on Jun 26, 2025 • 0 new comments
feat: `refine f ..` and `refine { a := 1, .. }`
#5525 commented on Jun 26, 2025 • 0 new comments
Git conflict experiment
#5500 commented on Jun 26, 2025 • 0 new comments
Add `\U00000000` notation for large unicode literals
#5443 commented on Jun 26, 2025 • 0 new comments
fix: consistently show non-mvar term in hovertext
#5368 commented on Jun 26, 2025 • 0 new comments
feat: qsort with proven bounds and correctness proof
#5346 commented on Jun 26, 2025 • 0 new comments
feat: propagate mvars out of `withNewMCtxDepth`
#5341 commented on Jun 26, 2025 • 0 new comments
feat: primitive profiling for slow isDefEq problems
#5318 commented on Jun 26, 2025 • 0 new comments
chore: rename 13 simp lemmas
#5317 commented on Jun 26, 2025 • 0 new comments
feat: use StateT.run instead of function application
#5121 commented on Jun 26, 2025 • 0 new comments
feat: add debug.sorryProps
#5091 commented on Jun 26, 2025 • 0 new comments
chore: bump olean version
#5089 commented on Jun 26, 2025 • 0 new comments
feat: allow `change` to capture subexpressions
#5063 commented on Jun 26, 2025 • 0 new comments
feat: create CACHEDIR.TAG file in .lake directory
#5059 commented on Jun 26, 2025 • 0 new comments
fix: make `rcases` tactic collect new goals
#5024 commented on Jun 26, 2025 • 0 new comments
doc: mention maxSteps setting in its error message
#3287 commented on Jun 26, 2025 • 0 new comments
feat: enforce indentation of command contents
#3215 commented on Jun 26, 2025 • 0 new comments
fix: make lean4 build on FreeBSD
#3182 commented on Jun 26, 2025 • 0 new comments
feat: lake: `require` overhaul
#3174 commented on Jun 26, 2025 • 0 new comments
refactor: lake: API cleanup / mark some defs `private`
#3166 commented on Jun 26, 2025 • 0 new comments
feat: profile instructions on Linux
#3161 commented on Jun 26, 2025 • 0 new comments
feat: make constructor tactic fail in ambiguous cases
#3127 commented on Jun 26, 2025 • 0 new comments
feat: optimize computing `BinderInfo`s for discrimination trees
#3113 commented on Jun 26, 2025 • 0 new comments
feat: basic `#lang`
#3101 commented on Jun 26, 2025 • 0 new comments
feat: error on non-rfl dsimp args
#3087 commented on Jun 26, 2025 • 0 new comments
fix: pass CMAKE_C/CXX_COMPILER to all stages
#3080 commented on Jun 26, 2025 • 0 new comments
feat: allow `EStateM` to be used universe-polymorphically
#3010 commented on Jun 26, 2025 • 0 new comments
(experimental) fix: match `MonadControlT` to `MonadControl`
#2944 commented on Jun 26, 2025 • 0 new comments
feat: Implement `extends flat`
#2940 commented on Jun 26, 2025 • 0 new comments
feat: adjust `dsimp` behavior (experimental)
#2910 commented on Jun 26, 2025 • 0 new comments
fix: don't write padding bits to olean files
#2908 commented on Jun 26, 2025 • 0 new comments
feat: set_option for conv mode
#2887 commented on Jun 26, 2025 • 0 new comments
perf: use pointer equality at kernel `inferType` and `whnf` caches (WIP)
#2782 commented on Jun 26, 2025 • 0 new comments
chore: decrease priority for `MonadError`
#4223 commented on Jun 26, 2025 • 0 new comments
chore: add minimization for 'dsimp at' issue
#4198 commented on Jun 26, 2025 • 0 new comments
feat: test for simp problem
#4171 commented on Jun 26, 2025 • 0 new comments
chore: CI: optimize code under Linux Debug
#4118 commented on Jun 26, 2025 • 0 new comments
feat: `lake install`
#3998 commented on Jun 26, 2025 • 0 new comments
feat: Implement Functor for Array
#3976 commented on Jun 26, 2025 • 0 new comments
feat: use `rfl` proofs of `Iff` in `dsimp`
#3973 commented on Jun 26, 2025 • 0 new comments
feat: binary recursive implementation of List.mapA
#3877 commented on Jun 26, 2025 • 0 new comments
chore: upstream `Nat.binaryRec`
#3756 commented on Jun 26, 2025 • 0 new comments
feat: BitVec.flatten and basic API
#3727 commented on Jun 26, 2025 • 0 new comments
feat: make `registerLabelAttr` consistent with `registerTagAttribute`
#3699 commented on Jun 26, 2025 • 0 new comments
feat: [WIP] Persistent env extension custom types
#3687 commented on Jun 26, 2025 • 0 new comments
fix: remove special handling of numerals in `DiscrTree`
#3684 commented on Jun 26, 2025 • 0 new comments
feat: `modifyM`/`modifyGetM` for `IO.Ref`
#3641 commented on Jun 26, 2025 • 0 new comments
fix: handle delayed-assigned mvars in `isDefEq` safely
#3637 commented on Jun 26, 2025 • 0 new comments
feat: `--continue-on-error` to produce .olean file even if elaboration fails
#3568 commented on Jun 26, 2025 • 0 new comments
fix: `isDefEq` handling of delayed-assigned mvars when `withAssignableSyntheticOpaque` is `true`
#3473 commented on Jun 26, 2025 • 0 new comments
chore: upstream Std's linter framework
#3291 commented on Jun 26, 2025 • 0 new comments

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

June 19, 2025 – June 26, 2025

Overview

Could not load contribution data

111 Pull requests merged by 20 people

19 Pull requests opened by 13 people

12 Issues closed by 6 people

11 Issues opened by 8 people

291 Unresolved conversations

Insights: leanprover/lean4

June 19, 2025 – June 26, 2025

Overview

Could not load contribution data

111 Pull requests merged by 20 people

19 Pull requests opened by 13 people

12 Issues closed by 6 people

11 Issues opened by 8 people

291 Unresolved conversations