I&#39;d say no. The current behavior means that somehow the unification mechanism is seeing through the abstraction? I&#39;d like to be able to prove see-through, but opaque violates abstraction, in my opinion.<div class="gmail_extra">
<br><br><div class="gmail_quote">On Thu, Nov 15, 2012 at 6:33 PM, Andreas Abel <span dir="ltr">&lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
If you have an abstract definition<br>
<br>
  abstract<br>
  Â  lhs = rhs<br>
<br>
is it ok with the meaning of `abstract&#39; that<br>
<br>
  lhs == rhs<br>
<br>
holds propositionally outside the abstract block. Â Agda currently says yes, but would you agree with Agda?<br>
<br>
  abstract<br>
<br>
  Â  T : Set -&gt; Set<br>
  Â  T A = A<br>
<br>
  Â  see-through : âˆ€ {A} â†’ T A â‰¡ A<br>
  Â  see-through = refl<br>
<br>
  opaque : âˆ€ {A} â†’ T A â‰¡ A<br>
  opaque = see-through<br>
<br>
Cheers,<br>
Andreas<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
Andreas Abel Â &lt;&gt;&lt; Â  Â  Â Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</font></span></blockquote></div><br></div>