Data.Witness.ListElement

Documentation

class HasListElement n list where

Minimal complete definition

getListElement, putListElement

Associated Types

type ListElement n list :: *

Methods

getListElement :: NatType n -> list -> ListElement n list

putListElement :: NatType n -> ListElement n list -> list -> list

Instances

HasListElement Zero (a, r)

Associated Types

type ListElement (Zero :: Nat) (a, r) :: *

Methods

getListElement :: NatType Zero -> (a, r) -> ListElement Zero (a, r)

putListElement :: NatType Zero -> ListElement Zero (a, r) -> (a, r) -> (a, r)

HasListElement n r => HasListElement (Succ n) (a, r)

Associated Types

type ListElement (Succ n :: Nat) (a, r) :: *

Methods

getListElement :: NatType (Succ n) -> (a, r) -> ListElement (Succ n) (a, r)

putListElement :: NatType (Succ n) -> ListElement (Succ n) (a, r) -> (a, r) -> (a, r)

modifyListElement :: HasListElement n t => NatType n -> (ListElement n t -> ListElement n t) -> t -> t