def Hex.GraphIso.Nauty.Sparse.Literal.range (first last : Nat) : List Nat

The same bounded traversal as the production range. Its list recursor has an exported body, so it also computes in an importing module's kernel.

Equations

• Hex.GraphIso.Nauty.Sparse.Literal.range first last = List.range' first (last - first)

theorem Hex.GraphIso.Nauty.Sparse.Literal.range_forIn {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (first last : Nat) (a : α) (f : Nat → α → m (ForInStep α)) : forIn (range first last) a f = forIn [first:last] a f