lean4

lean4 copied to clipboard

Replace `String.fromUtf8Unchecked` with `String.fromUtf8?`

3

Unlike `String.fromUtf8Unchecked`, this one should check for valid UTF-8. In fact, since we have to decode the string anyway to figure out its character length, we might as well remove...

Kha

docstring style guide

1

Leo asked for help from the community to write docstrings in the Lean 4 codebase. It would be nice to have a docstring style guide to help in this effort...

PatrickMassot

[RFC] Collapsible traces with messages

10

This PR contains a number of improvements to trace messages, most notably collapsible trace nodes can now have a message. Before (neovim screenshot): ``` [Meta.synthInstance] ▼ [Meta.synthInstance] main goal R...

gebner

Currently `Server.RequestM` does not provide any way to make a server->client LSP request and then wait on the client's response. This is useful in cases where we want to make...

Vtec234

Interleaved expected output in leantest_csimpAttr.lean?

3

### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean4/issues). *...

lovettchris

Term goals only sometimes show type class instances

20

```lean example [Inhabited Empty] : α := (default : Empty).rec --^ term goal (instance missing) example [Inhabited α] : α := default --^ term goal (instance shown) example [Inhabited α]...

gebner

connect maxHeartbeats in CoreM to kernel variable max_heartbeats

4

bollu

bollu

This is an implementation of labeled break and continue in do notation. ```lean example : IO Unit := do for (label := xLoop) x in [1:10] do for (label :=...

digama0

fix: translate `macro/elab` parameters `x:c` to `$x:c` instead of `$x`

2

This ensures `x` is guaranteed to be of kind `c` even in presence of partial syntax.

Kha