def ckr.le_by

bend-osdev-acpi@0.1.2.0 · PROOF_rsdp.bend:144

import Base
import bend-osdev-bytes@0.1.1.1/bytes.bend as B

144def ckr.le_by(+n: Nat, +o: B.Octets, +m: Nat, +e: {B.Octets.len(o) == m : Nat}, +h: {Nat.is_le(n, m) == True{} : Bool}) -> {Nat.is_le(n, B.Octets.len(o)) == True{} : Bool}:
145  %Equal.sym(Nat, B.Octets.len(o), m, e) : {Nat.is_le(n, _) == True{} : Bool}
146  h