def outcome_steps

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

import Base
import bend-osdev-acpi@0.1.1.0/aml_host.bend as Hs
import bend-osdev-acpi@0.1.1.0/aml_interp.bend as I
import bend-osdev-acpi@0.1.1.0/aml.bend as A

2538# an outcome counts the steps of its run
2539def outcome_steps(+r: I.AmlRun<Hs.AmlMemHost>) -> {I.AmlRun.steps(Hs.AmlMemHost, r) == A.AmlOutcome.steps(Hs.AmlMemHost, A.AmlOutcome.of_run(Hs.AmlMemHost, r)) : Nat}:
2540  match r:
2541    case I.AmlRun{m, s}:
2542      match m:
2543        case I.AmlMachine{md, c, fs, w}:
2544          match w:
2545            case I.AmlWorld{ctx, ns, h, e}:
2546              match e:
2547                case I.AmlEnv{wd, o, nts, d, cl}:
2548                  {==}