law gen_row_out

minebender-game@1.0.0.0 · proof_gen.bend:144

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

144law gen_row_out:
145  for +z: G.Zone
146  for +y: Nat
147  for +xs: List<&2, Nat>
148  for +j: Nat
149  for +st: G.GenState
150  for e: {List.get(&2, Nat, xs, j) == None{} : Maybe<&2, Nat>}
151  {List.get(&2, Bool, G.gen.row(z, y, xs, st), j) == None{} : Maybe<&2, Bool>}