Sebastian Ullrich
Sebastian Ullrich
I have a language server (https://github.com/leanprover/lean4) that uses `Hover.range?` to highlight term structure, e.g. hovering over `+` in `a + b` highlights the entire term. While this works well in...
I have a GH Actions workflow where I'm trying to configure a local binary cache restored from actions/cache, as that is quite a bit faster than always querying Cachix: ```...
It is not too hard to make Lean produce thousands of error messages, at least when working on the core lib. This can noticeably slow down editors (flycheck outright disables...
As witnessed in [formalabstracts](https://github.com/rlewis1988/formalabstracts/blob/30c0eca8448b83415c9dad991cb2ad625e00e8cd/fabstract/Bauer_A_InjBaireNat/realizability.lean#L8). I can think of multiple workarounds to this: * The one used in the link above and only one currently working: use any other command in...
```lean #check _ → a -- unknown identifier 'a' run_cmd tactic.to_expr ```(_ → a) >>= tactic.trace -- Π (a : Sort ?), a ``` In my specific case, the implicit...
Environments such as [idris-mode](https://github.com/idris-hackers/idris-mode) allow interacting with code in error messages. Ideally, we would like to provide the same set of interactions in code in messages and info views as...
It makes sense to keep going in server mode, but less so when building the stdlib.
As noticed in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Changing.20instance.20priority/near/292252231
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...
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...