Sebastian Ullrich
Sebastian Ullrich
Yeah, I was wondering if our language server was going against the spec while filing this issue! But it only says "is used to visualize a hover, e.g. by changing...
From a quick glance at VS Code, it looks like the hover is cached there at least inside a "word". That's not supported by the spec either, but probably harmless...
Looks like that works, interesting. Being able to use `extra-substituters` still would be a little nicer.
Electrolysis is using Lean 2, I should probably mention that in the readme. Porting it to Lean 3 would not be a small endeavor, and so will probably not happen...
Yes, types with interior mutability are outside the thesis' language subset a priori. Some of them like `Rc` could still be modeled in a referentially transparent way as long methods...
This is not a bug but a feature request for a missing set of APIs that can work with these "special" local constants (called `local_decl_ref`s in the C++ code) derived...
We could add a new special type `solve1_itactic` which we handle just like `{ tac }` (for which we already special-case the error position); I don't see a nice pure-Lean...
> We can do something very close in pure Lean using the cur_pos parser: we could use the position after the closing brace as the default position. I tried something...
Right, I was considering using a blank lines heuristic for that as well at some point. I'm not sure any code would break right now (could be an interesting experiment),...
> I think if we just forbid it after , it would already be good enough. Ok, sounds very reasonable.