[Agda] equality reasoning and contradictory type indices

[Nils Anders Danielsson]

On 2010-03-15 16:28, Chris Casinghino wrote:
> agda gives this error message if you ask it to case split on the
> result of the comparison:
>
>   Cannot pattern match on constructor less, since the inferred indices
>   [m2, suc (m2 + k2)] cannot be unified with the expected indices [m1
>   + k1, m1] for some <...> when checking that the expression ? has
>   type foo1 ≡ (foo2 | pat)

If the indices cannot be unified, then one can often move forward by
abstracting over some of the indices (either using with or a helper
function). In this case you may want to abstract over m1 + k1.

--
/NAD