lean4

lean4 copied to clipboard

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

TwoFX

Support for mutual and nested inductive types as `DecidableEq` instance generator

1

We currently have to manually write `DecidableEq` instances for nested and mutual inductive datatypes. Here is an example. ```lean namespace Example inductive Min where | Base | Const (a :...

leodemoura

RFC: try-this widget: multiple replacemens, alternative text in InfoView

1

### Proposal #### Multiple edits I would be able to address #4546 in maybe the most preferable way if the the “Try this” functionality would allow multiple simultaneous replacements. In...

nomeata

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

fonqL

``` import Lean example (range : String.Range) : String.Pos := ⟨range.stop.b⟩ example (p : String.Pos) : String.Pos := ⟨p.b⟩ ``` Both `b`s complete to very different lists, but neither contains...

Kha

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

TwoFX

RFC: built in option to suppress compilation of defs

1

### Proposal Add a built in option to disable compilation. [Here](https://github.com/leanprover/lean4/commit/c02bcb6b679eed0f7a7c2f812d63ac3b06a15ed6) is one possibility. (Edit: this is too naive.) - **User Experience**: Currently, Lean attempts to compile declarations in `noncomputable...

mattrobball

lake: redundant missing import errors

1

Here is an example failing build of Mathport due to a moved upstream file: ``` $ lake build ✖ [63/1717] Running Mathlib.Init.ZeroOne error: no such file or directory (error code:...

digama0

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

TwoFX

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

fonqL