@dpwiz I was thinking more of Idris, but you're right, its a stretch to call it a theorem prover