[Agda] again `with' vs `case'

Nils Anders Danielsson nad at cse.gu.se
Wed Sep 4 10:45:08 CEST 2013

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.


More information about the Agda mailing list