This is a very ad-hoc implementation of a Hoare triple prover,
following C.A.R. Hoare's classic paper "An Axiomatic Basis for Computer Programming".
Its original purpose is to serve as a demo ina reading course on "Classical Papers in Computer Science".
The original example from the paper can be found in Example.agda
The code type checks with Agda v2.6.3 and version 1.7.2 of Agda's standard library.