law set_full

lawful-arrays@0.1.0.0 · LAWS.bend:90

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

90law set_full:
91  for -T: Data
92  for a: Array<T>
93  for d: Nat
94  for i: U32
95  for v: T
96  for hf: {D.full(T, a, d) == True{} : Bool}
97  {D.full(T, Array.set(T, a, i, v), d) == True{} : Bool}