PROOF.seg_kind: def of bend-osdev-acpi@0.1.1.0
Import: import bend-osdev-acpi@0.1.1.0/PROOF.bend as PROOF
Lines 2056-2058 of bend-osdev-acpi@0.1.1.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&start_line=2056&end_line=2058

import Base
import bend-osdev-acpi@0.1.1.0/aml_name.bend as N

# a NameSeg's first byte is a LeadNameChar
def seg_kind(+c0: U32, +c1: U32, +c2: U32, +c3: U32, +ok: {N.nm.seg_ok4(c0, c1, c2, c3) == True{} : Bool}) -> {N.AmlLSeg{} == N.AmlLead.classify(c0) : N.AmlLeadKind}:
  is_seg_t(N.AmlLead.classify(c0), and_l(N.AmlLead.is_seg(N.AmlLead.classify(c0)), Bool.and(N.AmlName.name_char(c1), Bool.and(N.AmlName.name_char(c2), N.AmlName.name_char(c3))), ok))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=and_l
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=is_seg_t
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=AmlLead.classify
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=AmlLead.is_seg
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=AmlLeadKind
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=AmlName.name_char
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=nm.seg_ok4