[Agda] again `with' vs `case'

Nils Anders Danielsson nad at cse.gu.se
Tue Aug 27 13:31:56 CEST 2013

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.


More information about the Agda mailing list