Steve Dunham

So, with the example above, I'm getting these logs ``` LOG elab:10: Checking application of Main.case block in blah ($resolved2512) to [f@(BarA)] Rig Rig1 Function type (0 f : (Main.Bar...

> I added tentative PR's for the two failing CI: > > * [Frex #66](https://github.com/frex-project/idris-frex/pull/66) > * [Elab utils #39](https://github.com/stefan-hoeck/idris2-elab-util/pull/39) > > Both would need to be tweaked once this...

@ohad I think I might have that last case. I took my example: ```idris data Bar : Bool -> Type where BarA : Bar True BarB : Bar False test5...

Thanks for finding those issues. I think I have the first one fixed locally and am looking into the others, but I'm not sure the last two are correctly stated:...

> I understand (and my understanding can be wrong, of course) let q lhs = rhs as "pattern match rhs as lhs and limit all produced values to the quantity...

I've run through all of the combinations of variable quantity and case quantity. To the cases described above, I added ones where the variable was linear, but scrutinized at various...

I think we'll want to add a count to the case statement in the surface syntax (`PCase`). Should I do this here or save it for a separate PR? I'd...

The `IDRIS2_INC_CGS` environment variable asks Idris to build the .so files for all listed codegens whenever it builds the `.ttc` files. Internally, the `.ttc` files contain a list of incremental...

The man page says that the libc version of `getline` mallocs a buffer if null, and expects the caller to free it. Looks like openbsd requires a buffer to be...

It's reproducing for me with the 9.5 chez in ubuntu 20.04.3