What would be my best bet if I was aiming to eventually prove stuff about dependent types for Pikelet? Roll my own? Autosubst had an example for CC which looked neat and promising to my naive eye: https://ps.uni-saarland.de/autosubst/doc/Ssr.pred_CC_omega.html…
This Tweet was deleted by the Tweet author. Learn more
Oh cool, fingers crossed! Perhaps I'll try a prelease. It's understandable that they don't have as much funding to work with as other ecosystems, so I'm sympathetic in that regard. And even better that they are trying to improve things.