<div dir="ltr">Hi Sergei,<div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Can you, please, explain: what is the difference between writing</blockquote><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">... </blockquote><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">open import Relation.Binary.PropositionalEquality using (foo)<br>...<br>and</blockquote><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">... </blockquote><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">open import Relation.Binary.PropositionalEquality.Core using (foo)<br>...<br></blockquote><div><br></div><div>The former will have dependencies on all the imports listed at the top of `Relation.Binary.PropositionalEquality(.Algebra/Properties)` which includes the entire `Algebra` and `Relation.Binary` hierarchies. This can make it time consuming to load the module and increase the memory overhead.</div><div><br></div><div>The CHANGELOG wording perhaps needs updating for the full release, as users <a href="https://github.com/agda/agda-stdlib/blob/1309c75160e3125e1ce35b0b3db748821c75e22a/README.agda#L247">should not import `Core` modules directly</a>, and as we don't provide guarantees about their content.</div><div><br></div><div>Best,</div><div>Matthew</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Sep 1, 2020 at 3:27 AM <<a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On 2020-08-31 16:32, Matthew Daggitt wrote:<br>
> Dear all,<br>
> <br>
> The Agda Team is pleased to announce the first release candidate of<br>
> version 1.4 of the standard library.<br>
> [..]<br>
<br>
It is written there in CHANGELOG.md<br>
"<br>
  The module `Relation.Binary.PropositionalEquality` has been growing in <br>
size and<br>
  now depends on a lot of other parts of the library, even though its <br>
basic<br>
  functionality does not. To fix this some of its parts have been <br>
factored out.<br>
   `Relation.Binary.PropositionalEquality.Core` already existed. Added <br>
are:<br>
   ```agda<br>
   Relation.Binary.PropositionalEquality.Properties<br>
   Relation.Binary.PropositionalEquality.Algebra<br>
   ```<br>
These new modules are re-exported by <br>
`Relation.Binary.PropositionalEquality`<br>
and so these changes should be invisble to current users, but can be <br>
useful<br>
to authors of large libraries.<br>
"<br>
<br>
Can you, please, explain: what is the difference between writing<br>
module Foo where<br>
open import Relation.Binary.PropositionalEquality using (foo)<br>
...<br>
and<br>
module Foo Where<br>
open import Relation.Binary.PropositionalEquality.Core using (foo)<br>
...<br>
(assuming that foo is in ...Core)<br>
?<br>
Is the latter better for the authors of large libraries? Why?<br>
Do you mean that fewer modules of standard library will be type-checked?<br>
(because if PropositionalEquality is type-checked, then Agda needs to <br>
type-check<br>
at list once all the modules it imports).<br>
Does this make a difference to  Foo.agdai ?  its size?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
</blockquote></div>