lean4

lean4 copied to clipboard

digama0

Function coercion does not trigger if types require unification

2

As reported on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Regression.20in.20function.20coercion.20inference/near/303901188). This used to be supported in Lean 3 (community edition), and is used pretty heavily in mathlib: ```lean structure Equiv (α : Sort _) (β :...

gebner

Go-to-definition on typeclass method should go to instance

1

...while go-to-declaration should go to the typeclass as it does right now. I hope that's not too controversial (and may even have been suggested before)? Note that you can still...

Kha

Bump up to LLVM 15

2

Let us refactor the patch that adds LLVM support to Lean4 into another component: We first bump up LLVM to LLVM 15, and then add the bindings. We see that...

bollu

fix: improve fuzzy-matching heuristics

4

Closes #1546. There were no bugs with the current implementation as far as I could tell, but I noticed three areas that could be improved here: 1. Penalties should really...

rish987

fix: attribute info nesting

2

This fixes an issue with hovers inside user attributes caused by the fact that the info nodes generated by the user attribute are not nested correctly under the attribute itself,...

digama0

perf: garbage-collect dead sections

2

Benchmarks: https://github.com/leanprover/lean4/pull/1689#issuecomment-1268175703

Kha

no reviews yet please - #1494 - #1661 - #1662

EdAyers

feat: CodeActionProvider

2

This is a low-level system for registering LSP code actions. LSP code actions are editor integrated code actions. In VScode, you can trigger the `textDocument/codeAction` handler by hitting `Ctrl+.` (`Cmd+.`...

EdAyers

feat: track callers in panicking functions

8

This implements a feature similar to the `#[track_caller]` attribute in Rust or the `[HasCallStack]` typeclass in GHC Haskell. * The panicking primitive `panicWithPosWithDecl` and `panicWithPos` are changed to `StackInfo.panic` which...

digama0