law rows_wide_set

minebender-game@1.0.0.0 · proof_lists.bend:327

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/board.bend as B

327law rows_wide_set:
328  for -A: Data
329  for +w: Nat
330  for +g: T.Grid(A)
331  for +y: Nat
332  for +x: Nat
333  for +v: A
334  for +wide: {B.rows_wide(A, w, g) == True{} : Bool}
335  {B.rows_wide(A, w, List.set(&2, List<&2, A>, g, y, List.set(&2, A, row_of(A, g, y), x, v))) == True{} : Bool}