equalityagdadecidable

Looking for the Agda module that contains decidable equality for lists

Given two lists xs and ys, I would like to obtain a value of Dec(xs ≡ ys). Does any one know the name of the standard library module which contains such an operator?

Solution

  • It's in Data.List.Properties under the name ≡-dec