JAR: Join-Accumulate Refine

2.4. Sequences🔗

🔗def
Array.cyclicGet.{u_1} {α : Type u_1} (s : Array α) (i : Nat)
  (h : s.size > 0) : α
Array.cyclicGet.{u_1} {α : Type u_1}
  (s : Array α) (i : Nat)
  (h : s.size > 0) : α

Modular subscript: s[i]↻ ≡ s[i % |s|]. GP §3.7.

🔗def
Array.firstN.{u_1} {α : Type u_1} (s : Array α) (n : Nat) : Array α
Array.firstN.{u_1} {α : Type u_1}
  (s : Array α) (n : Nat) : Array α

First n elements: →s^n. GP §3.7.2.

🔗def
Array.lastN.{u_1} {α : Type u_1} (s : Array α) (n : Nat) : Array α
Array.lastN.{u_1} {α : Type u_1}
  (s : Array α) (n : Nat) : Array α

Last n elements: ←s^n. GP §3.7.2.

🔗def
IntRange (a b : Int) : Type
IntRange (a b : Int) : Type

ℤ_{a..b} : integers in [a, b). GP §3.4.