[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