Source code on Github
{-# OPTIONS --safe #-}
module Prelude.ToList where

open import Prelude.Init; open SetAsType
open import Prelude.Lists

record ToList (A : Type ) (B : Type ℓ′) : Type ( ⊔ₗ ℓ′) where
  field toList : A  List B
  _∙toList = toList
open ToList ⦃...⦄ public

private
  variable
    A : Type 
    B : Type ℓ′

instance
  ToList-List : ToList (List A) A
  ToList-List .toList = id

  ToList-List⁺ : ToList (List⁺ A) A
  ToList-List⁺ .toList = L.NE.toList

  ToList-Str : ToList String Char
  ToList-Str .toList = Str.toList

  ToList-Vec :  {n}  ToList (Vec A n) A
  ToList-Vec .toList = V.toList

  ToList-↦ :  {xs : List A}  ToList (xs  B) (A × B)
  ToList-↦ {xs = xs} .toList f = zip xs (codom f)