Data.Witness.List
- data ListType w a where
- NilListType :: ListType w ()
- ConsListType :: w a -> ListType w b -> ListType w (a, b)
- class HasListElement n list where
- type ListElement n list :: *
- getListElement :: Nat n -> list -> ListElement n list
- putListElement :: Nat n -> ListElement n list -> list -> list
- modifyListElement :: HasListElement n t => Nat n -> (ListElement n t -> ListElement n t) -> t -> t
Documentation
a witness type for HList-style lists. Here we use () and (,) for HNil and HCons.
The w parameter is the witness type of the elements.
Constructors
| NilListType :: ListType w () | |
| ConsListType :: w a -> ListType w b -> ListType w (a, b) |
Instances
| SimpleWitness w => SimpleWitness (ListType w) | |
| Representative w => Representative (ListType w) | |
| Eq1 w => Eq1 (ListType w) | |
| Representative w => Is (ListType w) () | |
| (Is w a, Is (ListType w) b) => Is (ListType w) (a, b) | |
| Eq1 w => Eq (ListType w a) |
class HasListElement n list whereSource
Associated Types
type ListElement n list :: *Source
Methods
getListElement :: Nat n -> list -> ListElement n listSource
putListElement :: Nat n -> ListElement n list -> list -> listSource
Instances
| HasListElement Zero (a, r) | |
| HasListElement n r => HasListElement (Succ n) (a, r) |
modifyListElement :: HasListElement n t => Nat n -> (ListElement n t -> ListElement n t) -> t -> tSource