Rohit Grover
Rohit Grover
@gallais: > In the meantime, if you're wondering how to get out of this predicament: > parametrise `MaybePreorder` over `rel`. Thanks for the suggestion. I'm still not out of this...
Thanks so much for investigating this. Your suggestions work, but I find it difficult to reason about them. Hopefully, Idris will do the right thing without requiring a workaround.
I wish to use cookies across requests. I am aware that a CookieJar can be obtained from a response. But to merge cookies across requests, I need `updateCookieJar` from Network.HTTP.Client....
@kindaro: Thanks. Yes, I am able to reuse the cookies returned in one response for the following request. The above is sufficient If all responses contained 'set-cookie' values for the...
This adds a dependency on readline. The CI system will need to be updated if this is to go ahead.
```idris foo4 : (1 f : (1 x : Nat) -> Maybe Char) -> Maybe Char foo4 f = Just (S Z) >>= (\arr => ?rhs arr) ``` The above...
The following rewrite doesn't give a type error: ```idris module Foo interface Foo a where bar : {auto ok: ()} -> a -> a ``` perhaps the implicit argument needs...
Could the style in https://github.com/edwinb/Idris2/blob/master/libs/base/Data/Nat.idr#L191 work for you?
```idris div : (n, d: a) -> Not (d = Semiring.zero) -> a ```
The following works: ```idris export sortBy : {n : Nat} -> (elem -> elem -> Ordering) -> Vect n elem -> Vect n elem sortBy _ [] = [] sortBy...