ProofCore.WD: def of lawful-bytes@0.1.1.0
Import: import lawful-bytes@0.1.1.0/proof_core.bend as ProofCore
Lines 26-28 of lawful-bytes@0.1.1.0/proof_core.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&start_line=26&end_line=28

import Base
import lawful-arrays@0.1.0.0/proof_tree.bend as P

# Word k of the block, as Array.get reads it.
def WD(+t: P.Tree<U32>, +k: U32) -> U32:
  Pair.snd(Array<U32>, U32, Array.get(U32, P.fromT(U32, t), k))

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_tree.bend&name=Tree
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_tree.bend&name=fromT