lean4

lean4 copied to clipboard

I expected to see that on this page/section of the doc https://leanprover.github.io/lean4/doc/organization.html but it isn't listed there

Seppel3210

Environment leaks between spawned processes (on Windows)

1

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

`elab_rules : tactic` patterns require redundant information

2

```lean import Lean syntax "foo " str : tactic open Lean Elab elab_rules : tactic | `(foo $x:str) => logInfo x.getString example : True := by foo "hello" -- Error...

leodemoura

We currently use the longest match parser combinator only when processing syntax categories. During the ICERM after-party hackton, users created fake "syntax category" to get the longest match behavior. BTW,...

leodemoura

No good way for proofs or local instances in theorem statements

5

In Lean 3 we had `by have : stmt := proof; exact term` which added `stmt` to the local context *without leaving any trace behind*. In Lean 4 `have` always...

gebner

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

PatrickMassot

@digama0 and I want to make sure tactics such as `Ring` can be invoked from `simp`.

leodemoura

Better support for browsing traces

7

This issue is a placeholder for collecting ideas and features for visualizing and filtering traces. @dselsam @Kha @Vtec234

leodemoura

Should head function syntax be hoverable?

1

Continuing discussion from [here](https://github.com/leanprover/lean4/issues/681#issuecomment-922544455) and #1157. There is currently an inconsistency between whether the head symbol in a function application is hoverable/selectable in source code and in the infoview. I...

Vtec234

Make the pretty printer usable for code formatting

5

The formatter in the pretty printer already produces pretty good output for goals and also makes a reasonable attempt at preserving comments and command-level layout: https://github.com/leanprover/lean4/blob/master/tests/lean/Reformat.lean.expected.out. But it is not...

Kha