This refactor simplifies much of the TC and content-addressing implementation by refactoring our constant representations in two main ways:
constructors no longer carry rhs, this is now left only with the recursor rules
we no longer distinguish between internal and external recursors on the TC side (a subtle difference remains on the IPLD side to account for the fact that internal recursors can have recursive reference)
TODO:
[x] Update Yatima/Ipld/PrimCids.lean
[x] Review the diff to make sure I didn't donk anything up on the merge
This refactor simplifies much of the TC and content-addressing implementation by refactoring our constant representations in two main ways:
rhs
, this is now left only with the recursor rulesTODO:
Yatima/Ipld/PrimCids.lean