Interactive theorem proving such as one provided by Agda is so empowering. The help provided by the compiler while interactively developing a proof is invaluable. Types guide you to a solution at every single step.
Interactive theorem proving such as one provided by Agda is so empowering. The help provided by the compiler while interactively developing a proof is invaluable. Types guide you to a solution at every single step.