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.
55
66* In accordance with changes to the flags in Agda 2.6.3, all modules that previously used
77 the ` --without-K ` flag now use the ` --cubical-compatible ` flag instead.
8-
8+
99* 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
122122 length (mapWith∈ xs f) ≡ length xs
123123 length-mapWith∈ [] = P.refl
124124 length-mapWith∈ (x ∷ xs) = P.cong suc (length-mapWith∈ xs)
125-
125+
126126 mapWith∈-id : ∀ xs → mapWith∈ xs (λ {x} _ → x) ≡ xs
127127 mapWith∈-id [] = P.refl
128128 mapWith∈-id (x ∷ xs) = P.cong (x ∷_) (mapWith∈-id xs)
You can’t perform that action at this time.
0 commit comments