def gen_first.found

minebender-game@1.0.0.0 · proof_gen.bend:227

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/game.bend as G
import minebender-game@1.0.0.0/LAWS.bend as L

227def gen_first.found(+z: G.Zone, +fx: Nat, +fy: Nat, +w: Nat, +g: T.Grid(Bool),
228  s: {G.gen.out(z, T.Pos{fx, fy}) == True{} : Bool},
229  r: Exists(G.GenState, st2 => {List.get(&2, List<&2, Bool>, g, fy)
230    == Some{G.gen.row(z, fy, List.range(w), st2)} : Maybe<&2, List<&2, Bool>>})) ->
231  {L.mine(g, T.Pos{fx, fy}) == False{} : Bool}:
232  match r:
233    case (st2, eq):
234      %Equal.sym(Maybe<&2, List<&2, Bool>>, List.get(&2, List<&2, Bool>, g, fy),
235        Some{G.gen.row(z, fy, List.range(w), st2)}, eq) :
236        {Maybe.default(&2, Bool, List.get(&2, Bool,
237          Maybe.default(&2, List<&2, Bool>, _, Nil{}), fx), False{}) == False{} : Bool}
238      gen_first.col(z, fx, fy, w, st2, s, Nat.is_lt(fx, w), {==})