def gen_bit_first

minebender-game@1.0.0.0 · proof_gen.bend:97

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

97def gen_bit_first(+z: G.Zone, +p: T.Pos, +st: G.GenState,
98  s: {G.gen.out(z, p) == True{} : Bool}) -> {G.gen.bit(z, p, st) == False{} : Bool}:
99  match st:
100    case G.GenState{need, left, rs}:
101      %Equal.sym(Bool, G.gen.out(z, p), True{}, s) :
102        {Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)), G.gen.pick(need, left, rs))
103          == False{} : Bool}
104      {==}