law size_tree

lawful-arrays@0.1.0.0 · proof_tree.bend:125

import Base
import lawful-arrays@0.1.0.0/defs.bend as D

125law size_tree:
126  for -T: Data
127  for +d: Nat
128  for +t: Tree<T>
129  for hf: {D.full(T, fromT(T, t), d) == True{} : Bool}
130  {Array.size(T, fromT(T, t)) == (fromT(T, t), U32.shln(1, d)) : Array<T> & U32}