[Agda] Colist -> List
Serge D. Mechveliani
mechvel at botik.ru
Tue Oct 2 15:20:03 CEST 2012
Please, how to convert Colist Char to List Char ?
I need to read a List Char from a file.
readFile returns IO Costring -- (Costring = Colist Char).
The program can extract coStr : Colist Char from this input.
But how to obtain List Char ?
I try
Colist.take :
forall {a} {A : Set a} (n : Nat) -> Colist A -> BoundedVec A n
:
module Main where
open import Data.Colist as Colist
open import Data.BoundedVec as BnVec
...
f : Costring -> BoundedVec Char 2
f coStr = Colist.take 2 coStr
And Agda-2.3.0.1 + MAlonzo + lib-0.6 reports
.Data.BoundedVec.Inefficient.BoundedVec Char 2 !=<
BoundedVec Char 2 of type Set
when checking that the expression Colist.take 2 coStr has type
BoundedVec Char 2
Just the same types of BoundedVec Char 2
are reported as different.
Can you explain this?
Thanks,
------
Sergei
More information about the Agda
mailing list