[Agda] about serialization

[Ulf Norell]

On Wed, Apr 5, 2017 at 3:35 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:

>
> This type can be defined as
>
> --------------------------------------------------------
> (let C =
>      .Relation.Binary.DecSetoid.Carrier (.Structures0.UpDSet.decSetoid
>         (.Structures0.UpMagma.upDSet
>         (.Structures0a.UpSemigroup.upMagma
>         (.Structures1.UpMonoid.upSemigroup
>         (.Structures1.UpCommutativeMonoid.upMonoid
>         (OverIntegralRing-0.*upCMon-NZ {α} {α=} upIR∣?)))))
>       )
>  in
>  {α α= : .Agda.Primitive.Level}
>  (upIR∣? : UpIntegralRing-with∣? α α=) →
>  Data.Product._×_ {α .Agda.Primitive.⊔ α=} {.Agda.Primitive.lzero}
>  C
>  .Agda.Builtin.Nat.Nat
>  →
>  C
> )
> -------------------------------------------------------
>
> But in the report the expression of C is printed twice.
> How the checker stores it internally?
>

It is stored twice. Some sharing is recovered during serialisation, but
it's not
represented explicitly so it will be destroyed by substitution.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170405/60105222/attachment.html>