[Agda] invert pattern matching

[Nils Anders Danielsson]

On 14/12/2018 21.57, Martin Escardo wrote:
> Thanks for explanation, Ulf. I understand what the error message means
> now. I had never got this error message before, and today I got it for
> the first time and then many times following this (when trying to give
> a term in a hole).

This is a warning, not an error. If you find it annoying, then you can
disable it:

   {-# OPTIONS --warning=noInversionDepthReached #-}

-- 
/NAD