Open mechvel opened 6 years ago
Yup at some point I'll get around to porting all the relevant proofs in Data.List.Properties
to Data.List.Relation.Equality.Setoid
.
But there is a more general condition for map f xs ≋ map g ys
, which is widely used:
map-pointwise-≈ : {f g : A → B} {xs ys : List A} → length xs ≡ length ys →
All id (zipWith (\x y → f x ≈ g y) xs ys) →
map f xs ≋ map g ys
Here B is the carrier of a setoid, which setoid exports ≈, and ≋ is the pointwise equality induced by ≈. Has lib-1.1 something for this?
Has lib-1.1 something for this?
No, nothing that general.
Yup at some point I'll get around to porting all the relevant proofs in
Data.List.Properties
toData.List.Relation.Equality.Setoid
.
Cf. #2360 / #2393 and discussion of module parametrisation in #2397 ... time to open a fresh issue with a roadmap/tasklist for "all the relevant proofs"?
Standard library provides map-cong, map-id, map-compose as related to the propositional equality ≡. But the case of List over Setoid is highly usable. And I suggest this: