Ohad Kammar

What would it take for sirdi to package itself? If we have a clear list of tasks to complete or decisions to make, maybe we can spread the effort among...

# Steps to Reproduce ```idris failing "Undefined name c." Fails : (xs : List a) -> List a Fails [] = [] Fails (x :: xs) with (length xs) Fails...

# Steps to Reproduce ```idris record Bar (a : Type) where constructor MkBar a : Nat ``` # Expected Behavior Depends on language design. Either: * type-check fine, and be...

Incorrect rejection of erased irrefutable patterns

6

(spotted by locria) # Steps to Reproduce ```idris f : (0 x : (a,b)) -> Nat f x = let 0 (u,v) = x in 0 ``` # Expected Behavior...

Auto search cuts too early when an earlier auto variable is solved

1

# Steps to Reproduce ```idris import Data.SnocList.Quantifiers as SnocList import Data.SnocList.Elem as SnocList data SType = A | B Context : Type Context = SnocList SType data Term : {ctx:...

Local definitions in irrelevant definitions are incorrectly checked for relevance

4

I thought we discussed/reported this at some point, but I can't find the report/fix. # Steps to Reproduce ```idris $ cat Irrel.idr 0 foo : (0 b : Bool) ->...

Segfault when displaying a hole

7

Sorry this is a large program. I'm happy to try to cut it down to a minimal example, but I really have no clue where to start. If you have...

Totality annotations are ignored

3

# Steps to Reproduce run `idris2 totality.idr` where [totality.idr](https://gist.github.com/ohad/8b30fb464769fd5ba76e4e086ea1d4ae) is: ``` total foo : a foo = foo ``` # Expected Behavior ``` - + Errors (1) `-- totality.idr line...

Whitespace-sensitive parsing of let binding without ascription

1

Sorry if this is a feature! # Steps to Reproduce Type-check the following declarations: ``` x1 : Nat x1 = let u = S Z in 1 x2 : Nat...

Module import unstable

5

I'm not sure this is a bug, it's possible my types are not quite right, or that I've used access modifiers the wrong way. # Steps to Reproduce Download the...