law row_in_len

minebender-game@1.0.0.0 · proof_lists.bend:234

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

234law row_in_len:
235  for -A: Data
236  for +w: Nat
237  for +h: Nat
238  for +g: T.Grid(A)
239  for +y: Nat
240  for +sh: {B.shaped(A, w, h, g) == True{} : Bool}
241  for yh: {Nat.is_lt(y, h) == True{} : Bool}
242  {List.length(&2, A, row_of(A, g, y)) == w : Nat}