A very simple example of verification in Idris | Heykuki News