Denis Buzdalov

Regression in #3328, compilation now hangs sometimes

2

# Steps to Reproduce Consider these functions: ```idris import Data.Fin covering g : Fin 64 -> Unit g FZ = () g (FS i') = g $ weaken i' total...

[multitimer] Timer cannot be set over the day end

1

### Affected hardware version Bangle 2 ### Your firmware version 2v25 ### The bug ### The bug When timer is being set to the point in time which must be...

`typebind` operators seems to have too narrow translation

1

Pinging @andrevidela as probably the only implementor of the feature # Steps to Reproduce Consider a couple of non-standard typebind operators `op` and `op'` and their non-typebind equivalents `po` and...

Inconsistent behaviour of linear quantity on function definitions

3

# Steps to Reproduce Consider the following function: ```idris 1 f : (1 _ : Nat) -> Nat f x = S x ``` It doesn't really matter what exactly...

[ Proposal ] Search only appropriate operator

4

I think the current determination of appropriate operators during desugaring is inconsistent. This PR tries to fix it. I'll try to explain my point. Basically, we can look at four...

[ discussion ] Pull typed TOML management out

1

I find typed TOML files management in `pack` (mostly in module `Pack.Core.TOML`) fascinating and usable not only in `pack`. I'd suggest universal parts (i.e. parts that do not touch specific...