law size_node_eq

lawful-arrays@0.1.0.0 · proof_shape.bend:14

import Base

14law size_node_eq:
15  for -T: Type
16  for -xs: Array<T>
17  for -ys: Array<T>
18  for -b: Array<T>
19  for -n: U32
20  for e: {Array.size(T, xs) == (b, n) : Array<T> & U32}
21  {Array.size(T, ANode{xs, ys}) == (ANode{b, ys}, U32.shl(n)) : Array<T> & U32}