[Agda] invert pattern matching

[Martin Escardo]

On 15/12/2018 16:11, nad at cse.gu.se wrote:
> 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 #-}

Thanks. I didn't find it annoying at all. I just wondered what it meant, 
and Ulf explained it very well.

Martin