2 ms·
Basically, the way it works is that the compiler prevents you from calling functions like head, tail and remove unless it has a proof that the list is non-empty
by fiddlerwoaroof 8y ago
Basically, the way it works is that the compiler prevents you from calling functions like head, tail and remove unless it has a proof that the list is non-empty.