lean4
lean4 copied to clipboard
leanprover
Lean 4 programming language and theorem prover
### 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). *...
This makes the `foo` in `syntax (name := foo) ...` act like a declaration name for the purpose of hovers (so by hovering on it you can see the rendered...
* [x] depends on #1478 * [ ] depends on #1483 This attribute allows you to specify another declaration to copy the docstring for the given declaration from. Example: ```lean...
Adds support for attributes on `macro`, `elab`, `macro_rules`, `elab_rules`. For `macro` and `elab` the attributes only apply to the `syntax` definition, not the `macro_rules` / `elab_rules` auxiliary definition along with...
As discussed in [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60lean.20--stdin.60.20does.20not.20respect.20Ctrl.2BD/near/292550058), this implements the blocking behavior seen by Rust. When a stream sees an EOF on a readLine, it will return an empty string once. When called...
As noticed in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Changing.20instance.20priority/near/292252231
```lean syntax "repro" (ident)? ident : command example : Lean.Syntax → Option Lean.Syntax | `(repro $[$x:ident]? a) => x --^ textDocument/hover | `(repro $[$x:ident]? b) => x --^ textDocument/hover --^...
tl;dr: https://twitter.com/famontesi/status/1557346899610443782 We already have both the state before and after a tactic in the info tree, we should use them at the same time! A full diff is probably...
- [x] waiting on https://github.com/leanprover/lean4/pull/1460 to include a `JsonNumber.fromFloat`
Metadata
Owner
Metadata
Lean 4 programming language and theorem prover