def tb.l64

bend-osdev-acpi@0.1.1.0 · PROOF_tables.bend:38

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-bytes@0.1.1.0/LAWS.bend as BL

38def tb.l64(+v: W.W64) -> {Nat.is_le(8n, B.Octets.len(B.Octets.le64(v))) == True{} : Bool}:
39  %Equal.sym(Nat, B.Octets.len(B.Octets.le64(v)), 8n, BL.octets_len_le64(v)) : {Nat.is_le(8n, _) == True{} : Bool}
40  {==}