~/jendhub

def size_w.node

lawful-arrays@0.1.0.0 · proof_shape.bend:28

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

28def size_w.node(-T: Type, -xs: Array<T>, ys: Array<T>, w: SizeW(T, xs)) -> SizeW(T, ANode{xs, ys}):
29  (b, n, e, q) = w
30  (ANode{b, ys}, U32.shl(n), size_node_eq(T, xs, ys, b, n, e), P.anode_eq(T, b, ys, xs, ys, q, {==}))

Uses (6)

Used by (1)