Stefan Höck

I have to think about this. Right now, `Property` is just a wrapper around `PropertyT ()`, which is itself a wrapper around ```idris EitherT Failure (WriterT Journal Gen) () ```...

Just for your info: I am working on a larger update where it is possible to run single tests (pure ones and tests running in `IO`). A PR will follow...

I haven't used `Promises` a lot so far, so I don't really have an opinion or a solution here. You could have a look at how they do this at...

What about going the other way, and wrap the possibility of failure into the value stored in the `Promise` itself: ```idris then' : Promise a -> (a -> JSIO (NS...

Yes, we definitely need this (and other ways for custom installations).

I think the same style should be used throughout the code base. I have accustomed myself to using the style you see in the code, which is used in all/most...

Sorry, I probably was too negative in my last comment, especially since I just now realized what the actual difficulty is: We can't see, whether an argument is an auto-implicit...

I have thought again about this after all the talk on Discord. Here's my suggestion: ```idris module Style import Data.IORef import Data.SortedMap foo : HasIO io => {auto ref :...

Thanks for the detailed answer. I was asking for your opinion in particular because you started this discussion by opening this issue. I can see your points - they are...

I have looked at those SOP articles before, but only superficially. I'm not sure, however, whether we have the necessary metaprogramming machinery for that in Idris2. Do you have any...