def reg_go_d

bend-osdev-acpi@0.1.1.0 · PROOF.bend:2409

import Base
import bend-osdev-acpi@0.1.1.0/error.bend as E
import bend-osdev-acpi@0.1.1.0/header.bend as H
import bend-osdev-acpi@0.1.1.0/registry.bend as R

2409def reg_go_d(+reg: R.AcpiRegistry, +r: Result<&2, &2, E.AcpiError, H.AcpiSdt>, +t: R.AcpiTable<R.AcpiNoExt>, +e: {R.reg.go(~R.AcpiNoExt, ~R.AcpiNoExt.parse, reg, r) == Done{t} : Result<&2, &2, E.AcpiError, R.AcpiTable<R.AcpiNoExt>>}) -> {Result.is_done(&2, &2, E.AcpiError, H.AcpiSdt, r) == True{} : Bool}:
2410  match r:
2411    case Fail{x}:
2412      Empty.absurd({Result.is_done(&2, &2, E.AcpiError, H.AcpiSdt, Fail{x}) == True{} : Bool}, fd_absurd(R.AcpiTable<R.AcpiNoExt>, x, t, e))
2413    case Done{x}:
2414      {==}