-
Notifications
You must be signed in to change notification settings - Fork 235
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
comments on lib-2.1 candidate 1 #2415
Comments
Re: (3) see the discussion on #2378 As to eta and epsilon, these are conventional names from category theory, and the properties follow from the self-adjunction introduced in the PR. But as above, they are left as comments because they amount to (no more than) yet more synonyms for lemmas originally defined in |
Re: (1) The introduction of Our more recent approach for
Relying on 'monotonic' behaviour of |
Re: (2) |
With lib-2.0 it worked , for example, a) Users (like myself) may have a thousand occurrences of this to be changed in the user code. |
|
What example are you talking of?
Under lib-2.1-rc1 the report is "Unsolved metas", (Built with flags (cabal -f) - optimise-heavily, |
As to the nature of the 'bug':
Reversion to the status quo ante (eg by reverting commit 438f9ed, although that unfortunately touches both the new definitions in |
I do not understand the details you are talking of. |
Indeed. #2365 changed the implementation of a suite of functions including, but not only, |
(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
Agda 2.6.4.3 Built with flags (cabal -f)
the type check keys are "--auto-inline --guardedness"
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
But there are also needed
(you can change the implementation).
Here
reverse⁺
is renamed toreverse∈⁺
in order to avoid clash withreverse⁺
for⊆
.(3.2)
"NB. the unit and counit of this adjunction are given by:"
Eta and epsilon do not look clear here to many people.
Is not it better to call them
xs⊆reverse-xs
andreverse-xs⊆xs
and to provide the implementation directly?
The text was updated successfully, but these errors were encountered: