~/jendhub

def ckr.lt_by

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

import bend-osdev-acpi@0.1.2.0/PROOF_rsdp.bend as PROOFRsdp
import Base
import bend-osdev-bytes@0.1.1.1/bytes.bend as B

148def ckr.lt_by(+n: Nat, +o: B.Octets, +m: Nat, +e: {B.Octets.len(o) == m : Nat}, +h: {Nat.is_lt(n, m) == True{} : Bool}) -> {Nat.is_lt(n, B.Octets.len(o)) == True{} : Bool}:
149  %Equal.sym(Nat, B.Octets.len(o), m, e) : {Nat.is_lt(n, _) == True{} : Bool}
150  h

Uses (6)

Used by (1)