<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Feb 5, 2016 at 9:13 AM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 05.02.2016 08:34, Ulf Norell wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Without cheating, I would expect<br>
<br>
module M Γ where<br>
record R Δ<br>
<br>
to yield the same types for functions and projections as<br>
<br>
module M where<br>
record R Γ Δ<br>
</blockquote>
<br></span>
But this means that inside M, there are declarations that do not have the module telescope Gamma as a prefix, but the hiding-modified one.<br>
<br>
For instance,<br>
<br>
module M (A : Set) where<br>
record R : Set where<br>
data D (a : A) : Set where<br>
open R public<br>
data E (a : A) : Set<br>
<br>
then<br>
<br>
E = M.E Nat<br>
<br>
is ok while<br>
<br>
D = M.D Nat<br>
<br>
will give a type error?<br></blockquote><div> </div><div>Yes.</div><div><br></div><div>/ Ulf</div></div></div></div>