def size_w

lawful-arrays@0.1.0.0 · proof_shape.bend:32

import lawful-arrays@0.1.0.0/proof_shape.bend as ProofShape

import Base

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

Uses (4)

Used by (2)