You write something, Agda2 checks it and says that you forget something, you wrote an inconsistent code or you wrote ambiguous code (it is possible to hide some parts of code).
You write something, Agda2 checks it and says that you forget something, you wrote an inconsistent code or you wrote ambiguous code (it is possible to hide some parts of code).