Pure, Declarative, and Constructive Arithmetic Relations (Declarative Pearl)