Edwin Brady

**Comment by [edwinb](https://github.com/edwinb)** _Saturday Dec 07, 2019 at 15:13 GMT_ ---- I've labelled this with "Feature request" - we ought to have them really. If anyone wants pointers on where...

We don't eta expand records (yet?) so I'd expect this.

**Comment by [edwinb](https://github.com/edwinb)** _Sunday Jul 28, 2019 at 12:17 GMT_ ---- Internally, these exist, but there's no syntax yet. There is a possible complication - implicits might appear in a...

**Comment by [clayrat](https://github.com/clayrat)** _Sunday Jul 28, 2019 at 13:31 GMT_ ---- Yeah I think going for a simpler solution and assuming a fixed order might be good enough for a...

Given that we check the scrutinee of the with block before generating the type, thus knowing what it uses, I wonder if we could do better about generating the type...

This is certainly because it's pulling the two `x`s from the type to be in scope on the LHS. I suppose the thing to do is to only add one....

`case` is dependent, and it doesn't have enough information to infer the expected type if you don't use it, given that inference for dependent types is undecidable. I know it's...

This isn't anything to do with vim mode, but rather idris itself. Interactive editing requires there to be an idris instance running, with the file being edited being in its...

What are the steps to reproduce this? Does it happen every time? Have you tried, for example, deleting all .ibcs and checking that there's no other idris running? I know...

Any ideas how to persuade vim to do this? Is vimscript expressive enough? As you can probably tell from the interactive bits of vim mode, my knowledge of vimscript is...