Gabriel Ebner

> Here's what I've got on my device at commit ce5ca7: Thanks so much for running the tests! I'll take a look at `leanittest_complete_trailing_period.lean`. > (btw it failed at first...

> Based on the comment, I assume this may be an issue for @gebner? The comment just means that this has been on (the end of) my todo list for...

> Which I'd very much hope is none of them in practice. I'm pretty sure that neovim completely ignores the version field (and doesn't set `versionSupport` at all). VSCode explicitly...

Another interesting primitive is `Promise`, which allows you to create a `Task` whose value is provided later by calling `Promise.resolve`. This connects the "poll-based" world of tasks with the "push-based"...

@ydewit Thanks for the references! If you look closely the split is already there: `Promise` is the producer and `Task` is the consumer. The proposed API is essentially the same...

There is another syntax now which is hard to hover: `a[i]`. There are two one-character ranges that show the full term.

I agree with Mario that showing this as a code lens is only useful for extreme cases. And then it shouldn't be based on wall-clock measurements, but on heartbeats. (How...

Incidentally, I have disabled all code lenses in all languages because I think they're extremely annoying and only take up precious vertical space, except for one: the version lens extension...

> A signature is not a valid term syntax But it can be valid syntax in another (adhoc) category. This is certainly not the only case where we want to...

> It's been a while since I looked at this so maybe I am missing something, but it isn't clear to me why we'd want this in the current setup,...