~/jendhub

def opening_in

minebender-game@1.0.0.0 · proof_gen.bend:321

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

321# A wide zone holds every cell next to the first click.
322def opening_in(+first: T.Pos, +p: T.Pos, +wide: Bool, ew: {wide == True{} : Bool},
323  near: {L.within_one(first, p) == True{} : Bool}) -> {G.gen.out(G.Zone{first, wide}, p) == True{} : Bool}:
324  %Equal.sym(Bool, wide, True{}, ew) : {G.gen.out(G.Zone{first, _}, p) == True{} : Bool}
325  Equal.trans(Bool, B.within_one(first, p), L.within_one(first, p), True{}, within_eq(first, p), near)

Uses (9)

Used by (1)