Description
(1) Visibility of Data.Product.zipWith
Checking ForTests (/home/mechvel/inAgda/doconA/3.2/source/ForTests.agda).
Multiple definitions of zipWith.
Previous definition at
/home/mechvel/agda/stLib/2.1-rc1/src/Data/List/Base.agda:83,1-8
when scope checking the declaration
open import Data.Product public hiding (map; zip)
Is this backwards compatible?
(2) What is the matter with
Data.List.Properties.filter-accept, filter-reject ?
Unlike with lib-2.0, it appears "Unsolved", and it requires implicit
arguments to be set
- this is under the same type checker
Agda 2.6.4.3 Built with flags (cabal -f)- optimise-heavily,
the type check keys are "--auto-inline --guardedness"
- optimise-heavily,
And it occurs non-backwards compatible.
The effect often occurs that Agda silently hangs forever, then one has to guess and search for filter-accept in the currently processed module.
My program has probably thousand of places where the implicit arguments filter-accept/reject need to be inserted.
After this is fixed, the whole my application works.
I wonder of why the effect is produced while the type checker version is the same and the function definition is the same.
Can you explain the effect?
(3) reverse and ⊆.
lib-2.1-rc1 has in Data.List.Relation.Binary.Subset.Setoid.Properties
reverse-selfAdjoint : as ⊆ reverse bs → reverse as ⊆ bs
reverse⁺ : as ⊆ bs → reverse as ⊆ reverse bs
reverse⁻ : reverse as ⊆ reverse bs → as ⊆ bs
But there are also needed
reverse-preservesʳ-⊆ : ∀ {xs} → rev Preserves (xs ⊆_)
reverse-preservesʳ-⊆ {xs} {ys} xs⊆ys = xs⊆rev-ys
where
xs⊆rev-ys : xs ⊆ (rev ys)
xs⊆rev-ys = reverse∈⁺ S ∘ xs⊆ys
reverse-preservesˡ-⊆ : ∀ {xs} → rev Preserves (_⊆ xs)
reverse-preservesˡ-⊆ {xs} {ys} ys⊆xs = rev-ys⊆xs
where
rev-ys⊆xs : (rev ys) ⊆ xs
rev-ys⊆xs {z} z∈rev-ys = ys⊆xs z∈ys
where
revrev-ys≡ys = reverse-involutive ys
z∈revrev-ys : z ∈ rev (rev ys)
z∈revrev-ys = reverse∈⁺ S z∈rev-ys
z∈ys = subst (z ∈_) revrev-ys≡ys z∈revrev-ys
(you can change the implementation).
Here reverse⁺ is renamed to reverse∈⁺ in order to avoid clash with reverse⁺ for ⊆.
(3.2)
"NB. the unit and counit of this adjunction are given by:"
reverse-η : ∀ {xs} → xs ⊆ reverse xs
reverse-η = Membershipₚ.reverse⁺ S
reverse-ε : ∀ {xs} → reverse xs ⊆ xs
reverse-ε = Membershipₚ.reverse⁻ S
Eta and epsilon do not look clear here to many people.
Is not it better to call them xs⊆reverse-xs and reverse-xs⊆xs
and to provide the implementation directly?