ProofGen.zone: def of minebender-game@1.0.0.0 Import: import minebender-game@1.0.0.0/proof_gen.bend as ProofGen Lines 70-72 of minebender-game@1.0.0.0/proof_gen.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_gen.bend&start_line=70&end_line=72 import Base import minebender-game@1.0.0.0/types.bend as T import minebender-game@1.0.0.0/game.bend as G # The zone a board of n mines keeps free around the first click. def zone(+w: Nat, +h: Nat, +n: Nat, +first: T.Pos) -> G.Zone: G.Zone{first, Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h))} Uses (6): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=Zone https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos