2 ms·
That is the dependent typed aspect mentioned. This is actually done in Idris with VerifiedSemigroup and other verified instances.
by reuben364 10y ago
That is the dependent typed aspect mentioned. This is actually done in Idris with VerifiedSemigroup and other verified instances.
- Bromskloss 10y agoOK. I'm afraid I don't know enough to make the connection. Actually, I never understood the point of dependent types. They seem to do away with the neat order that types introduce. ¯\_(ツ)_/¯