Polysemy.Internal.Index

Documentation

class InsertAtIndex (index :: Nat) (head :: [k]) (tail :: [k]) (oldTail :: [k]) (full :: [k]) (inserted :: [k]) where

Infer a partition of the result type full so that for the fixed segments head and tail, the new segment inserted contains the missing effects between them.

Methods

insertAtIndex :: SList inserted

Instances

inserted ~ ('[] :: [k]) => InsertAtIndex index (head :: [k]) (oldTail :: [k]) (oldTail :: [k]) (full :: [k]) (inserted :: [k])

Defined in Polysemy.Internal.Index

Methods

insertAtIndex :: SList inserted

(InsertAtIndex index head tail oldTail full insertedTail, inserted ~ (e ': insertedTail)) => InsertAtIndex index (head :: [a]) (e ': tail :: [a]) (oldTail :: [a]) (full :: [a]) (inserted :: [a])

Defined in Polysemy.Internal.Index

Methods

insertAtIndex :: SList inserted