[Agda] An error function and totality

[Nils Anders Danielsson]

On 19/11/2018 07.30, Marko Dimjašević wrote:
> Does Agda have an equivalent function?

If you compile programs using the GHC backend, then postulates are
(currently) turned into uses of the error function.

-- 
/NAD