An attempt at explaining Decidable Equality
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.
Tue, 15 Mar 2022