[Agda] An error function and totality

[Marko Dimjašević]

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:

https://hackage.haskell.org/package/base-4.12.0.0/docs/Prelude.html#v:e
rror

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

https://www.idris-lang.org/docs/1.2/base_doc/docs/Debug.Error.html

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


-- 
Regards,
Marko Dimjašević <marko at dimjasevic.net>
https://dimjasevic.net/marko
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>