the joy of watching introductory videos about dependently typed purrogramming languages like Idris is you will inevitably encounter rather thorough discussions about the succ