Mathew Polzin
Mathew Polzin
In preparation for a v4.0.0 release, I am bumping this issue to the v5.x milestone.
I've used many of these proofs extensively in `rewrites` which don't require them to reduce at compile time so mostly out of curiosity would you mind providing a motivating example...
that sounds like a reasonable solution as long as you don't need to omit any relationships (really, anything outside of `attributes`) conditionally. just cuz the `hidden/0` function only operates on...
Multi line comments are supported and have at least at times worked so this is a compiler bug rather than a documentation bug. Worth fixing I’m guessing at least for...
Oh yeah, I misunderstood your comment and misread the example. My bad!
@stefan-hoeck this issue is good to get closed if you'd like. Not only was it ultimately an upstream issue but the problem was fixed by https://github.com/idris-lang/Idris2/pull/3386 as well.
The question is a bit vague for me to know exactly what the end goals are, but there are several potential answers depending on those goals. If you want to...
Just a small update: it's been a bit now since `pack` was made available as a package in nixpkgs. It can be installed in the normal way under NixOS now....
Interesting. But if you’re using the pack database (via the pack executable or, for example, my idris2Packages pack collection), then the mismatch the article refers to does not exist. All...
My initial thought was that this feels like an unfortunately manual tool for the task that would lead to a lot of the “darn, I need that too, better update...