type ContentReady

stelliferous@0.0.2.0 · proofs/storage_buffer_model.bend:32

import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape

32type ContentReady<-Element: Data,-content: Content<Element>> is Data:
33  ContentReady{depth: Nat,balanced: Shape.Balanced(Element,depth,content_tree(~Element,content)),
34    depth_ok: {Nat.is_le(depth,30n) == True{} : Bool},
35    room: {Nat.is_le(content_length(~Element,content),U32.to_nat(Tree.capacity(Element,content_tree(~Element,content)))) == True{} : Bool}}