G. Allais
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...