Thomas Ekström Hansen
Thomas Ekström Hansen
Home
Recent posts
Experience
Accomplishments
Blog
Coursework
Light
Dark
Automatic
formal-methods
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.
Thomas Ekström Hansen
Tue, 15 Mar 2022
Cite
×