Intro

A brief (ish) overview of common terminology and syntax used in FP, with the aim of getting you to think in words rather than weird symbols.

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.