22 Jan
2023
22 Jan
'23
9:59 p.m.
... rewrite rules for type constraints ...
That's what FunDeps are, with the advantage you can stipulate multiple/multi-directional rewrites. (With a bit of effort you can support three FunDeps for `Nat` Plus.) The more I think about it, the more it seems type-land 'solving' is not the same job as term-land 'evaluating'; and Type Families are the wrong tool for the job. AntC