def ready_content

stelliferous@0.0.2.0 · proofs/storage_buffer_model.bend:88

import Base
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape

88def ready_content(~Element: Data,+model: Model<Element>,evidence: ContentReady<Element,content(~Element,model)>) -> Sized<Element,model>:
89  Model{+tree,+length,Certificate.Certificate{+depth,+equation}} = model
90  ContentReady{+proved_depth,proved_balanced,depth_ok,room} = evidence
91  Sized{
92    %Equal.sym(Nat,depth,proved_depth,Shape.unique_depth(Element,tree,depth,proved_depth,balanced(~Element,model),proved_balanced)) : {Nat.is_le(_,30n) == True{} : Bool} depth_ok,
93    room}