[Agda] equality reasoning and contradictory type indices

[Chris Casinghino]

Thanks Nils!  This suggestion has helped me move forward.

--Chris

On Mon, Mar 15, 2010 at 1:28 PM, Nils Anders Danielsson
<nad at cs.nott.ac.uk> wrote:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>