G. Allais

AFAIU this is more a problem of seeing an existing `.ttc` and loading it despite the fact it has been generated from the `.idr` and not the `.lidr` file. What...

I have a love/hate relationship with this proposal. But mostly love.

I expect `foo` is the one that would be implicitly bound as it is the one in [argument position](https://github.com/edwinb/Idris2/blob/master/src/TTImp/Utils.idr#L17).

> Isn't it possible to at least have an `Eq Type` instance now so this can be done via a with clause? You can write a simulator `run(M,n)` running a...

In Agda, the goals' context is simply listing the renamed variables which is not very helpful. The goal itself however (or rather: any telescope) explicitly mentions the user-provided name and...

Is function composition not adequate in this situation? ```idris getNestedSubElement : MyRecord -> Nat getNestedSubElement myRec = subElement . nested $ myRec ``` If you want to go left-to-right, you...

> Error in TTC file: TTC data is in an older format, file: ["Prelude"], expected version: 21, actual version: 20 You have old `ttc` files lying around so you should...

It could be because of all of the `*.ttc` stored in `~/.idris2`. I usually use `find . -name "*.ttc"` to find them. And then you can go nuclear with `find...

The issue is that `(a, b)` can stand both for the pair type of `a` & `b` or the pair of values `a` & `b` whose type is a pair...

Do we gain much by using pygment rather than outputting e.g. markdown to be post-processed by pandoc? Re, looking at rendered examples we can use htmlpreview.github.io. See for instance: [your...