Commit ff61ad5
[ refactor ] Refactor and optimize
* [ refactor ] Replace `rev` with `reverse` and make `LengthMatch` arguments erased
* [ refactor ] Move `embed'` definition into `FreelyEmbeddable` implementation
* [ refactor ] Optimize `mkPatClause.mkNames` in `CaseBuilder`
* [ refactor ] Swap parameters of `NamedPats`
* [ refactor ] Remove `snoc` for `NamedPats`
* [ refactor ] Use `List` for forward order in `CaseBuilder.idr`
* [ refactor ] Swap the arguments of `PatClause`, `Group` and `ScoredPats` like `NamedPats`
* [ refactor ] Merge simillar cases in `nextNames'` and `mkNames`
* [ cleanup ] Remove redudant functions
Cherry-picked from GulinSS#16
Fully authored by Viktor Yudov <[email protected]>
Co-authored-by: Viktor Yudov <[email protected]>CaseBuilder (#16)1 parent 9aad6cf commit ff61ad5
File tree
6 files changed
+339
-379
lines changed- src
- Core
- Case
- Name
- TT
- Libraries/Data/SnocList
- TTImp/Elab
6 files changed
+339
-379
lines changed
0 commit comments