Contents

Definition

Given a type $M$ and a sequence $x:\mathbb{N} \to M$ of terms in $M$, the left shift operator

is defined as

for $i:\mathbb{N}$.

See also

• sequence
• right shift operator
• sequential derivative