Open L-as opened 1 year ago
The proofs can in hindsight be made much more elegant. Performance also needs to be considered, everything that can be represented as an integer should be an integer. Many GADTs should be made into fully erased data families too.
Existential types would help a shit ton. Should probably be made a priority.
The proofs can in hindsight be made much more elegant. Performance also needs to be considered, everything that can be represented as an integer should be an integer. Many GADTs should be made into fully erased data families too.