Sequences

• $ %e : seq T$

  empty

  
  
• $ _ |> _ : seq T \* T -> seq T$

  right append

  
  
• $ _ <| _ : T \* seq T -> seq T$

  left append

  
  
• $ _ \. _ : seq T \* seq T -> seq T$

  concatenation

  
  
• $<< _ >> : T -> seq T$

  lifting

  
  
• $<< _,...,_ >> : T^{n} -> seq T$

  multiple arguments

  
  

• $G_{seq T } = { %e, |> }$, $GU_{seq T } = { %e, %e |> a, %e |> b, ..., %e |> a |> b, ... }$
• $G'_{seq T } = { %e, <| }$, $GU'_{seq T } = { %e, a <| %e , b <| %e, ..., b <| a <| %e, ... }$
• $G''_{seq T } = { %e, \. , << _ >> }$, $GU''_{seq T } = { %e, <>, <>, ,..., %e \. %e, ..., %e \. <> , ... }$