Formal-Methods

One of the more difficult concepts in Idris, I’ve found, is proving things through dependent types. The ‘simplest’ introduction to this is probably the DecEq interface, which this post aims to introduce, explain, and implement.