ProofGen.nr: def of minebender-game@1.0.0.0 Import: import minebender-game@1.0.0.0/proof_gen.bend as ProofGen Lines 902-904 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=902&end_line=904 import Base import minebender-game@1.0.0.0/board.bend as B # x is within one step of a. def nr(+a: Nat, +x: Nat) -> Bool: Nat.is_le(B.dist(a, x), 1n) Uses (4): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=dist