def ckr.le6

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

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

102def ckr.le6(+oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}) -> {Nat.is_le(Nat.add(0n, 6n), B.Octets.len(oem)) == True{} : Bool}:
103  %Equal.sym(Nat, B.Octets.len(oem), 6n, oem6) : {Nat.is_le(Nat.add(0n, 6n), _) == True{} : Bool}
104  {==}