Serge S. Gulin

hm, I've tried to track the changes but [this commit](https://github.com/mjustus/Idris2/commit/3578f703cc66160aca0a07526744a41f3797f49c) is unclear for me. Could you put more info there? @gallais @mjustus

@gallais @mjustus FYI Not-so-trivial rebase may occur [here](https://github.com/idris-lang/Idris2/pull/3626)

@gallais @mjustus Might be better to merge current refactor progress "as is"?

> The new academic year is about to start so unfortunately I don't think I'll be able to come back to this for a while. I mean I could take...

I've collected commits from https://github.com/mjustus/Idris2/commit/3578f703cc66160aca0a07526744a41f3797f49c, then added holes to make it compilable as is to see the needed surface to fix. Applied trivial fixes. Working on filling holes.

@mjustus @gallais I've rolled out your refactor intentions over the full codebase and now it compiles just fine, see CI. Actually it only compiles now, not work. My next steps...

Short list of all test errors ATM: ``` idris2/basic/basic055 base/data_bits001 contrib/list_alternating chez/channels008 chez/chez004 chez/integers chez/chez032 chez/chez027 refc/buffer refc/integers refc/strings node/node024 node/node004 node/integers ``` Unfortunately, I am unable to reproduce them...

Took into consideration @gallais points where I did replacements where it should not be. Also asked @buzden how to determine where such replacements should be and should not be. He...

Well, I am in progress ``` 229/286: Building Core.Case.CaseBuilder (src/Core/Case/CaseBuilder.idr) ```

It compiles! The next steps are to 1. group all changes by their semantics 2. groke translate rules from `cons` to `snoc` style 3. apply them. Starting work on the...