Denis Buzdalov

Maybe not fold the only top-level section

3

If a document has a single top-level section (e.g., a title of a document), it seems, it's better to not to fold it because the first thing you do in...

# Steps to Reproduce ```idris %default total interface S where pop : {_ : Unit} -> Unit S where pop = ?fooo ``` The signature may have an `auto`-implicit parameter...

# Steps to Reproduce Set `CHEZ` environment variable to something that does not start with a slash (`/`) and compile an application. # Expected Behavior Either successsfull compilation or nice...

# Steps to Reproduce Typecheck the following code ```idris import Data.DPair f : Exists List -> Unit f = \(Evidence _ _) => () ``` in an editor with semantic...

Local `pack.toml`s are very useful in setting desired requirements, especially when something non-standard needs to be reproducible, say when we ship a repository to, say, a customer. But sometimes we...

Currently the design decision is that all options must go before the command name. But since shell completion script uses only the current and the previous words, it cannot tell...

# Steps to Reproduce Consider I have a file `Main.idr` with the following contents: ```idris namespace XX export main : IO () main = putStrLn "Hi, XX!" namespace YY export...

Typechecker complains that it can't match on erased argument when it actually can

3

# Steps to Reproduce Arguments with quantity `0` can be matched when they have the only constructor in the current context. E.g. this successfully typechecks: ```idris data Y : Bool...

[ base ] Deprecate `toList` functions for sorted sets and maps

2

# Description Both `Data.SortedMap` and `Data.SortedSet` have specialised `toList` functions. For `Data.SortedSet`, I think this is a historical curious case, since its signature and semantics completely copies `toList` from `Prelude`,...

# Steps to Reproduce Consider the following piece of code: ```idris v : (Nat, Nat) g : Unit g = do let xx@(x, y) = v let prf1 = the...