Unfortunately there is no complete way to convert from a Colist to a List, because a Colist is potentially infinite and you can't detect whether it is beforehand. The best you can do is decide on a "maximum depth" (a natural) and recurse over that to construct a list of at most that length. That's what the BoundedVec in your code is supposed to do. Your problem is that you imported the wrong one. You need to import Data.BoundedVec.Inefficient, which is the one that Colist.take uses. The one you imported is just an abstract interface.<div>
<br></div><div>Hope this helps!</div><div>Dan<br><br><div class="gmail_quote">On Tue, Oct 2, 2012 at 9:20 AM, Serge D. Mechveliani <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">Please, how to convert Colist Char to List Char ?<br>
<br>
I need to read a List Char from a file.<br>
readFile returns IO Costring -- (Costring = Colist Char).<br>
The program can extract coStr : Colist Char from this input.<br>
But how to obtain List Char ?<br>
I try<br>
Colist.take :<br>
forall {a} {A : Set a} (n : Nat) -> Colist A -> BoundedVec A n<br>
:<br>
module Main where<br>
open import Data.Colist as Colist<br>
open import Data.BoundedVec as BnVec<br>
...<br>
f : Costring -> BoundedVec Char 2<br>
f coStr = Colist.take 2 coStr<br>
<br>
And Agda-2.3.0.1 + MAlonzo + lib-0.6 reports<br>
<br>
.Data.BoundedVec.Inefficient.BoundedVec Char 2 !=<<br>
BoundedVec Char 2 of type Set<br>
when checking that the expression Colist.take 2 coStr has type<br>
BoundedVec Char 2<br>
<br>
Just the same types of BoundedVec Char 2<br>
are reported as different.<br>
Can you explain this?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>