An Agda encoding of the primitive imperative language IMP from Glynn Winskel's ‘The Formal Semantics of Programming Languages’.