<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Apr 5, 2017 at 3:35 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
This type can be defined as<br>
<br>
------------------------------<wbr>--------------------------<br>
(let C =<br>
     .Relation.Binary.DecSetoid.<wbr>Carrier (.Structures0.UpDSet.decSetoid<br>
        (.Structures0.UpMagma.upDSet<br>
        (.Structures0a.UpSemigroup.<wbr>upMagma<br>
        (.Structures1.UpMonoid.<wbr>upSemigroup<br>
        (.Structures1.<wbr>UpCommutativeMonoid.upMonoid<br>
        (OverIntegralRing-0.*upCMon-NZ {α} {α=} upIR∣?)))))<br>
      )<br>
 in<br>
 {α α= : .Agda.Primitive.Level}<br>
 (upIR∣? : UpIntegralRing-with∣? α α=) →<br>
 Data.Product._×_ {α .Agda.Primitive.⊔ α=} {.Agda.Primitive.lzero}<br>
 C<br>
 .Agda.Builtin.Nat.Nat<br>
 →<br>
 C<br>
)<br>
------------------------------<wbr>-------------------------<br>
<br>
But in the report the expression of C is printed twice.<br>
How the checker stores it internally?<br></blockquote><div><br></div><div>It is stored twice. Some sharing is recovered during serialisation, but it's not</div><div>represented explicitly so it will be destroyed by substitution.</div><div><br></div><div>/ Ulf</div></div></div></div>