lean4

lean4 copied to clipboard

Add option `pp.beta`

1

When `pp.beta` is set to `true`, the pretty-printer (delaborator) should apply beta reduction. Lean 3 implements this feature, but we had *not* implemented it yet in Lean 4.

leodemoura

Asynchronous printing hangs the server

5

### 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). *...

tydeu

### 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

Finish GMP removal

2

Kha

This is another unexpected RC operation I noticed while debugging the recent lsan false positive. If their RC is 1, neither the task closure nor its captured values should be...

Kha

### 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

Definition jumping to a local dependency seems to jump to the wrong path

5

### 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). *...

Julian

Kha

Suppress field names with default values during delaboration

1

The following example ```lean import Lean open Lean.Meta #check ({} : Context) ``` produces ```lean { config := { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox :=...

leodemoura

We have only one reduction strategy when checking definitional equality in the kernel. It uses the "lazy unfolding" and it is suboptimal for many applications. Examples: - Any application that...

leodemoura