JAR: JAM Axiomatic Reference

1.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.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.