[Agda] nontermination and Sized types

[vlad]

> My experience, as an occasional user of this stuff, is that `Size<` is
> broken, and you have to make do with `↑`, `_⊔_`, &c. This makes it a
> really bad thing that the example in the documentation uses `Size<` (if
> my impressions are correct).
>
> James
>
The Codata implementations in the standard library also use Size< quite 
extensively: they use Thunks, which use Size<.

I don't see any way of dealing with coinductive (record) definitions 
without Size<.  ↑ works for inductive definitions, because, e.g.,  one 
can write

     data list {A : Set}: { k : Size} →  Set where
           cons : ∀ {k} →  A → list{A} {k} → list{A} {↑ k}

However, for coinductive records, I don't see how to replace the Size< 
in the standard definition (below) by anything else:

     record stream{A : Set} {k : Size} : Set where
          coinductive
          field
             head : A
             tail :  {j : Size< k} → stream{A} {j}

I've tried a couple of things but got parsing or typechecking errors.  
Does anybody know a way to define the above without Size< ?

Best regards

- Vlad

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