law nth_replicate

bend-osdev-array@0.1.0.1 · LAWS.bend:244

import bend-osdev-array@0.1.0.1/LAWS.bend as LAWS
import Base
import bend-osdev-array@0.1.0.1/array.bend as A

244law nth_replicate:
245  for -T: Data
246  for n: Nat
247  for v: T
248  for k: Nat
249  for f: T
250  for h: {Nat.is_lt(k, n) == True{} : Bool}
251  {A.Arrays.nth(T, List.replicate(T, n, v), k, f) == v : T}

Uses (7)

Used by (0)

No other definition uses this definition.