law gen_row_len

minebender-game@1.0.0.0 · proof_gen.bend:14

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

14law gen_row_len:
15  for +z: G.Zone
16  for +y: Nat
17  for +xs: List<&2, Nat>
18  for +st: G.GenState
19  {List.length(&2, Bool, G.gen.row(z, y, xs, st)) == List.length(&2, Nat, xs) : Nat}