~/jendhub

def oc.len

bend-osdev-cbc@0.1.0.0 · PROOF.bend:34

import bend-osdev-cbc@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-mode-core@0.1.0.0/LAWS.bend as CoreL

34def oc.len(+o: B.Octets, +n: Nat, h: {B.Octets.len(o) == n : Nat}) -> {B.len(B.Octets.to_list(o)) == n : Nat}:
35  CoreL.octets_len(o, n, h)

Uses (6)

Used by (1)