Ohad Kammar

@gallais @dunhamsteve Does the`RigCount` on `ICase` need to be a `Maybe RigCount`? We don't always know the ambient rigcount during desugaring, and maybe that means we need to keep guessing...

I'm glad you pushed to github --- means we get to talk about it :).

You can already use the cons syntax directly: ```idris foo :: bar :: baz :: quux :: Nil ```

Question for the review: Does the`RigCount` on `ICase` need to be a `Maybe RigCount`? We don't always know the ambient rigcount during desugaring, and maybe that means we need to...

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 PR is merged, so we'll probably...

I think the BarA example shadows the constructor with a freshly bound variable.

Can we please summarise (perhaps in the original description) which cases work and which don't, and make sure there's a remaining issue for each unintended non-compiling case?

@reswatson , this post is fascinating, but I don't quite see what it has to do with the practical question: what do we do about all the stuff that's in...

An undercurrent in this discussion is 'what's the alternative?'. Being in `contrib` means your package is way more discoverable and installable than any other alternative. It also means that any...

It's only anticlassical if you put LEM in the proof-relevant fragment. It might not be anticlassical if you put it in a propositional fragment, no?