G. Allais
G. Allais
> However, a few solutions have been proposed and I don't think that deleting the module is the best one. I am not saying it's the best one but it...
IIUC this will require us to update the CI script that generates the docs automatically: https://github.com/idris-lang/Idris2/blob/45fc038300979a9e3ff7799e8c22f3fc80b4014d/.github/scripts/katla.sh#L23 Something like: ```diff - cp -r "$prefix"/"$libname"/build/docs/* html/"$libname" + cp -r "$prefix"/"$libname"/build/docs/"$libname"/* html/"$libname" ```
I don't know what to think. On the one hand it allows you to know the output you're looking at will only talk about that one package's content, on the...
The plan is for `contrib` to be slowly taken apart and disposed of. So I don't think I will accept PRs adding content to it.
I think it may be that Idris is too clever and moving `ev p` and `ev q` past `stepEv e` but it does not appropriately mangle the auxiliary LHSs to...
> Lazy values can be matched using Delay. This looks like a bug to me
You can write: ```idris data D : Type -> Type where C : D a f : D (Type -> Type) -> () f (C {a = .(Type -> Type)})...
I suspect this is #225
I tried to play the same game with `Acc` but luckily in that case the tree **is strict** and so we don't end up with an infinite loop when typechecking...
This is the exepected behaviour following the case-of-lambdas optimisation: https://github.com/idris-lang/Idris2/blob/6b38592b5ac12bb45d3fa825e143b3e838c064eb/src/Compiler/CaseOpts.idr#L17-L31 According to Edwin this helps chez producing faster code in general.