<div dir="ltr"><div dir="ltr"><div dir="ltr">You can define such a function yourself.<div><br></div><div>  postulate</div><div>    impossible : ⊥</div><div><br></div><div>or even</div><div><br></div><div>  postulate</div><div>    error : ∀ {A} → String → A</div><div><br></div><div>I find this ability useful. However, an attempt to normalise a term that depends on a postulate will yield a term in which the postulate appears rather than raising an error. It would be helpful if Agda had an option to raise an error in such circumstances, and to indicate in a file terms to be normalised to confirm they don't depend on such postulates. Yours, -- P</div><div><br clear="all"><div><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div><div>Too brief? Here's why: <a href="http://www.emailcharter.org/" target="_blank">http://www.emailcharter.org/</a></div></div></div></div></div></div><br></div></div></div></div><br><div class="gmail_quote"><div dir="ltr">On Mon, 19 Nov 2018 at 06:31, Marko Dimjašević <<a href="mailto:marko@dimjasevic.net">marko@dimjasevic.net</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear Agda community,<br>
<br>
I've been wondering if there is an Agda equivalent of the error<br>
function in Haskell and Idris. In Haskell, it is this one:<br>
<br>
<a href="https://hackage.haskell.org/package/base-4.12.0.0/docs/Prelude.html#v:e" rel="noreferrer" target="_blank">https://hackage.haskell.org/package/base-4.12.0.0/docs/Prelude.html#v:e</a><br>
rror<br>
<br>
In Idris, it is the Debug.Error.error function:<br>
<br>
<a href="https://www.idris-lang.org/docs/1.2/base_doc/docs/Debug.Error.html" rel="noreferrer" target="_blank">https://www.idris-lang.org/docs/1.2/base_doc/docs/Debug.Error.html</a><br>
<br>
I find it interesting that Idris reports this function to be total,<br>
although it throws an exception. I asked in the Idris mailing list how<br>
come it is total [1], but I got no reply in two weeks.<br>
<br>
Does Agda have an equivalent function? Does Agda find the function to<br>
be total?<br>
<br>
<br>
[1] <a href="https://groups.google.com/forum/#!topic/idris-lang/_CqBa0YZJSw" rel="noreferrer" target="_blank">https://groups.google.com/forum/#!topic/idris-lang/_CqBa0YZJSw</a><br>
<br>
<br>
-- <br>
Regards,<br>
Marko Dimjašević <<a href="mailto:marko@dimjasevic.net" target="_blank">marko@dimjasevic.net</a>><br>
<a href="https://dimjasevic.net/marko" rel="noreferrer" target="_blank">https://dimjasevic.net/marko</a><br>
PGP key ID:       056E61A6F3B6C9323049DBF9565EE9641503F0AA<br>
Learn email self-defense! <a href="https://emailselfdefense.fsf.org" rel="noreferrer" target="_blank">https://emailselfdefense.fsf.org</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>