Agda-2.5.1.2: A dependently typed functional programming language and proof assistant

The only exported function. It's (only) called in Main.hs.