ProofShape.size_w: def of lawful-arrays@0.1.0.0
Import: import lawful-arrays@0.1.0.0/proof_shape.bend as ProofShape
Lines 32-37 of lawful-arrays@0.1.0.0/proof_shape.bend: https://jend.leeeet.dev/read.txt?path=lawful-arrays@0.1.0.0/proof_shape.bend&start_line=32&end_line=37

import Base

def size_w(-T: Type, a: Array<T>) -> SizeW(T, a):
  match a:
    case ALeaf{x}:
      (ALeaf{x}, 1, {==}, {==})
    case ANode{xs, ys}:
      size_w.node(T, xs, ys, size_w(T, xs))

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_shape.bend&name=SizeW
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_shape.bend&name=size_w.node