law set_full

lawful-arrays@0.1.0.0 · proof_shape.bend:191

import Base
import lawful-arrays@0.1.0.0/defs.bend as D

191law set_full:
192  for -T: Type
193  for a: Array<T>
194  for +d: Nat
195  for +i: U32
196  for v: T
197  for hf: {D.full(T, a, d) == True{} : Bool}
198  {D.full(T, Array.set(T, a, i, v), d) == True{} : Bool}