law gen_rows_len

minebender-game@1.0.0.0 · proof_gen.bend:31

import Base
import minebender-game@1.0.0.0/game.bend as G

31law gen_rows_len:
32  for +z: G.Zone
33  for +w: Nat
34  for +ys: List<&2, Nat>
35  for +st: G.GenState
36  {List.length(&2, List<&2, Bool>, G.gen.rows(z, w, ys, st)) == List.length(&2, Nat, ys) : Nat}