[Agda] An error function and totality

[Marko Dimjašević]

Dear Philip,

On Mon, 2018-11-19 at 08:55 +0000, Philip Wadler wrote:
> 
> 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. 


Thank you for your reply. What you wrote sounds related to typed
holes. 

Is there a particular resource you would recommend for learning about
normalisation?


Kind regards,
Marko Dimjašević
-------------- 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/e3c678c3/attachment.sig>