Donovan Crichton
Donovan Crichton
I tried the following and it type checks just fine: ```idris f3 : (n : Nat) -> case n of Z => Vect Z Nat -> Vect (S Z) Nat...
Okay, so I had a brief look at this today. I can confirm that I cannot reproduce this bug if i replace `if ... then ... else` with `ifThenElse`. I...
Just confirming that I had this same issue and solved it by removing the `StrictData` extension from my cabal file. Thanks for writing this up!
I'm not very across the subtleties of linear types yet to be honest, so please bear with me while I clarify my understanding (and please point out anything I get...
Cheers @ziman and @andrevidela! Ok, so there's a lot of intuition I still don't have for linear types then. So I wont chime in too much here and leave it...
There might be some issues with shadowing going on with my previous example. Here it is again to be more specific: ```idris data MyList : Type -> Type where Nil...
Closed due to #2984