def ckw.lt01

bend-osdev-acpi@0.1.2.0 · PROOF_whole.bend:63

import Base
import bend-osdev-bytes@0.1.1.1/bytes.bend as B
import bend-osdev-bytes@0.1.1.1/LAWS.bend as BL
import bend-osdev-acpi@0.1.2.0/header.bend as H

63def ckw.lt01(+k: U32) -> {Nat.is_lt(0n, B.Octets.len(H.hd.byte(k))) == True{} : Bool}:
64  %Equal.sym(Nat, B.Octets.len(B.Octets.of_list([k])), B.len([k]), BL.octets_len_of_list([k])) : {Nat.is_lt(0n, _) == True{} : Bool}
65  {==}