ProofLaws.agrees_pick: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_laws.bend as ProofLaws
Lines 198-214 of minebender-game@1.0.0.0/proof_laws.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_laws.bend&start_line=198&end_line=214

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
import minebender-game@1.0.0.0/proof_base.bend as P
import minebender-game@1.0.0.0/proof_copy.bend as PC

def agrees_pick(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +p: T.Pos, +c: Bool, +m: Bool,
  me: {B.mine(layout, p) == m : Bool}) ->
  {L.agrees(w, h, layout, p, G.seen_pick(c, m, w, h, layout, p)) == True{} : Bool}:
  match c m:
    case False{} _:
      {==}
    case True{} True{}:
      %PC.mine_eq(layout, p) : {_ == True{} : Bool}
      me
    case True{} False{}:
      %PC.mine_eq(layout, p) :
        {Bool.and(Bool.not(_), Nat.is_eq(L.adj_mines(w, h, layout, p), B.adj_mines(w, h, layout, p))) == True{} : Bool}
      %Equal.sym(Bool, B.mine(layout, p), False{}, me) :
        {Bool.and(Bool.not(_), Nat.is_eq(L.adj_mines(w, h, layout, p), B.adj_mines(w, h, layout, p))) == True{} : Bool}
      %PC.adj_mines_eq(w, h, layout, p) :
        {Bool.and(True{}, Nat.is_eq(_, B.adj_mines(w, h, layout, p))) == True{} : Bool}
      P.eq_refl(B.adj_mines(w, h, layout, p))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=adj_mines
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=agrees
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=adj_mines
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=mine
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=seen_pick
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=eq_refl
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_copy.bend&name=adj_mines_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_copy.bend&name=mine_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Grid
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos