Ohad Kammar

I'm comfortable with moving cong and cong2 out of the prelude and into base.

I think the right places to start would be: ``` libs/prelude/Prelude/Num.idr ``` where you'll need to add binding for the primitive constants, and also the places where the primitives are...

Ah, sorry for misleading. I've removed my incorrect text.

I think the IDE protocol can be used to this effect. The protocol requests can be recorded with dependencies and their responses cached, and a simple compiler state flag can...

It's possible that the implementation is significantly different, but since this proposes a major overhaul of the compiler, I think the IDE protocol is a viable alternative that should be...

I guess the main point that @vfrinken makes is this: the current code is quite substantially broken, so someone does need to go through all the C FFI functions (in...

The IDE protocol supports a message for normalising a term. Can this proposed feature be reduced to normalise term (which isn't yet implemented in idris2)?

One example comes up in @madman-bob 's work on [tabular data](http://www.github.com/madman-bob/idris2-table). We have operations on tabular data that change the schema: ```idris result : Table ?hole result = join students...

So this issue has been opened just over 3 years ago, and it's stuck 'only' on syntax. We currently have the open proposal and discussion to revamp the named-application syntax...

When we were playing with this fragment, it looked like something got b0rked when lifting `f` to the top level during elaboration.