File tree Expand file tree Collapse file tree 2 files changed +2
-2
lines changed
src/Data/List/Membership/Setoid Expand file tree Collapse file tree 2 files changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -5,5 +5,5 @@ The library has been tested using Agda 2.6.3.
5
5
6
6
* In accordance with changes to the flags in Agda 2.6.3, all modules that previously used
7
7
the ` --without-K ` flag now use the ` --cubical-compatible ` flag instead.
8
-
8
+
9
9
* Updated the code using ` primFloatToWord64 ` - the library API has remained unchanged.
Original file line number Diff line number Diff line change @@ -122,7 +122,7 @@ module _ (S : Setoid c ℓ) where
122
122
length (mapWith∈ xs f) ≡ length xs
123
123
length-mapWith∈ [] = P.refl
124
124
length-mapWith∈ (x ∷ xs) = P.cong suc (length-mapWith∈ xs)
125
-
125
+
126
126
mapWith∈-id : ∀ xs → mapWith∈ xs (λ {x} _ → x) ≡ xs
127
127
mapWith∈-id [] = P.refl
128
128
mapWith∈-id (x ∷ xs) = P.cong (x ∷_) (mapWith∈-id xs)
You can’t perform that action at this time.
0 commit comments