Steve Dunham

Currently that is a parse error: ``` 1: Couldn't parse declaration. src.Temp:12:13--12:14 08 | -- then S (countFst (x :: zs) | zs) 09 | -- else countFst (x ::...

Because of this - it maybe parses a number and then decides its an error if there is a number there that is not 0 or 1. Arguably correct if...

I've [coded this up](https://github.com/idris-lang/Idris2/compare/main...dunhamsteve:Idris2:issue-3327?expand=1) and the type annotations are working fine, but I need to drop the multiplicities on the pattern matching version. We can still have quantities on bare...

Yeah, it's done. I don't think I had access to close other people's issues at the time, and I didn't have the right magic in the description to close it.