[Agda] again `with' vs `case'

[Nils Anders Danielsson]

On 2013-08-27 20:22, Sergei Meshveliani wrote:
> On Tue, 2013-08-27 at 13:31 +0200, Nils Anders Danielsson wrote:
>> On 2013-08-26 20:35, Sergei Meshveliani wrote:
>>> cong2-∈ {A = A} x (u ∷ xs) (v ∷ ys) (u=v ∷p =tail) x∈u-xs =
>>
>> Note that the left-hand side above is rejected, even if you replace the
>> right-hand side with a question mark.
>
> What does this mean "rejected" ?

Sorry, I was a bit imprecise. The clause by itself is not rejected, but
the entire definition is. Note that the coverage checker does not
inspect right-hand sides.

-- 
/NAD