Denis Buzdalov
Denis Buzdalov
Imagine you have selected some collection and have built a local package using `pack build` command. Its result now is stored in the `build` directory and uses current's compiler version...
# Context The fact that `Stream[F, O]` can be easily got from `Pull[F, O, Unit]` is severely used in this example. `Stream`'s bracket API does not allow the release action...
# Context We can use whatever we want as the only thing in idiom brackets, say a `Nat` or `String`: ```idris ff : List Nat ff = let x =...
# Steps to Reproduce Consider two functions with the same signature: ```idris r1 : a -> Stream a r1 x = xs where xs : Stream a xs = x...
According to #1436, we can't have a runtime-values of types like `forall a. List a -> Nat`. But consider we need to pass a list of types including one like...
# Steps to Reproduce Consider the following program ```idris main : IO () main = do printLn $ String.length "ab" printLn $ String.length "a\0b" ``` and run is with different...
This PR implements a _weak_ memoisation of lazy values for the chez backend **as an codegen option (directive)**. Weakness is in the fact that no guarantees of no re-evaluation of...
This issue looks really similar to #3158, but this issue, I think, is different. The #3158 is about particular backend, but this feature is about C FFI, available to (and...
# Steps to Reproduce Consider the folllowing code: ```idris import Data.Nat %default total conc : List a -> List a -> List a conc xs [] = xs conc xs...
# Steps to Reproduce Consider the following seemingly equivalent definitions: ```idris %default total incAll : Stream Nat -> Stream Nat incAll (x::xs) = S x :: incAll xs incAll' :...