[Agda] An error function and totality

Marko Dimjašević marko at dimjasevic.net
Mon Nov 19 07:30:42 CET 2018

Dear Agda community,

I've been wondering if there is an Agda equivalent of the error
function in Haskell and Idris. In Haskell, it is this one:


In Idris, it is the Debug.Error.error function:


I find it interesting that Idris reports this function to be total,
although it throws an exception. I asked in the Idris mailing list how
come it is total [1], but I got no reply in two weeks.

Does Agda have an equivalent function? Does Agda find the function to
be total?

[1] https://groups.google.com/forum/#!topic/idris-lang/_CqBa0YZJSw

Marko Dimjašević <marko at dimjasevic.net>
PGP key ID:       056E61A6F3B6C9323049DBF9565EE9641503F0AA
Learn email self-defense! https://emailselfdefense.fsf.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181119/5238329f/attachment.sig>

More information about the Agda mailing list