3 ms·
He explicitly gives standard machinery like the a boolean type and natural numbers, presumably to show more clearly what the parts are built up from. You probab
by Dewie3 11y ago
He explicitly gives standard machinery like the a boolean type and natural numbers, presumably to show more clearly what the parts are built up from. You probably wouldn't need to write all of that to use HList at a later point.
- danghica 11y agoYou would still need to program in Agda though :) Cheers!