def content_length_of

stelliferous@0.0.2.0 · proofs/storage_buffer_model.bend:56

import Base

56def content_length_of(~Element: Data,+model: Model<Element>) -> {content_length(~Element,content(~Element,model)) == length(~Element,model) : Nat}:
57  Model{tree,length,certificate} = model
58  {==}