Add lens module for strings

This commit is contained in:
Kiana Sheibani 2023-04-24 09:14:26 -04:00
parent 482edefd59
commit 2b16d484f5
Signed by: toki
GPG key ID: 6CB106C25E86A9F7

30
src/Data/String/Lens.idr Normal file
View file

@ -0,0 +1,30 @@
module Data.String.Lens
import Data.String
import Data.Profunctor
import public Control.Lens
import Data.List.Lens
%default total
public export
unpacked : Iso' String (List Char)
unpacked = iso unpack pack
public export
packed : Iso' (List Char) String
packed = iso pack unpack
public export
Ixed Nat Char String where
ix k = unpacked . ix k
public export
Cons String String Char Char where
cons_ = prism' (uncurry strCons) strUncons
public export
Snoc String String Char Char where
snoc_ = unpacked . snoc_ . mappingFst packed