We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent b5fc010 commit df0ea63Copy full SHA for df0ea63
CHANGELOG/v1.7.2.md
@@ -5,5 +5,5 @@ The library has been tested using Agda 2.6.3.
5
6
* In accordance with changes to the flags in Agda 2.6.3, all modules that previously used
7
the `--without-K` flag now use the `--cubical-compatible` flag instead.
8
-
+
9
* Updated the code using `primFloatToWord64` - the library API has remained unchanged.
src/Data/List/Membership/Setoid/Properties.agda
@@ -122,7 +122,7 @@ module _ (S : Setoid c ℓ) where
122
length (mapWith∈ xs f) ≡ length xs
123
length-mapWith∈ [] = P.refl
124
length-mapWith∈ (x ∷ xs) = P.cong suc (length-mapWith∈ xs)
125
126
mapWith∈-id : ∀ xs → mapWith∈ xs (λ {x} _ → x) ≡ xs
127
mapWith∈-id [] = P.refl
128
mapWith∈-id (x ∷ xs) = P.cong (x ∷_) (mapWith∈-id xs)
0 commit comments