diff --git a/CHANGELOG/v1.7.2.md b/CHANGELOG/v1.7.2.md index 0183ec654f..8ddea63b4d 100644 --- a/CHANGELOG/v1.7.2.md +++ b/CHANGELOG/v1.7.2.md @@ -5,5 +5,5 @@ The library has been tested using Agda 2.6.3. * In accordance with changes to the flags in Agda 2.6.3, all modules that previously used the `--without-K` flag now use the `--cubical-compatible` flag instead. - + * Updated the code using `primFloatToWord64` - the library API has remained unchanged. diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda index c72a782a42..888d10f5b7 100644 --- a/src/Data/List/Membership/Setoid/Properties.agda +++ b/src/Data/List/Membership/Setoid/Properties.agda @@ -122,7 +122,7 @@ module _ (S : Setoid c ℓ) where length (mapWith∈ xs f) ≡ length xs length-mapWith∈ [] = P.refl length-mapWith∈ (x ∷ xs) = P.cong suc (length-mapWith∈ xs) - + mapWith∈-id : ∀ xs → mapWith∈ xs (λ {x} _ → x) ≡ xs mapWith∈-id [] = P.refl mapWith∈-id (x ∷ xs) = P.cong (x ∷_) (mapWith∈-id xs)