law gen_rows_out

minebender-game@1.0.0.0 · proof_gen.bend:189

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

189law gen_rows_out:
190  for +z: G.Zone
191  for +w: Nat
192  for +ys: List<&2, Nat>
193  for +i: Nat
194  for +st: G.GenState
195  for e: {List.get(&2, Nat, ys, i) == None{} : Maybe<&2, Nat>}
196  {List.get(&2, List<&2, Bool>, G.gen.rows(z, w, ys, st), i) == None{}
197    : Maybe<&2, List<&2, Bool>>}