kuruczgy

set_option autoImplicit false
namespace Vk
abbrev FixedArray α (_ : Nat) := Array α
structure InstanceCreateFlags := private mk :: private v : UInt32
deriving DecidableEq
instance : HOr InstanceCreateFlags InstanceCreateFlags InstanceCreateFlags := ⟨(⟨·.v ||| ·.v⟩)⟩
instance : HAnd InstanceCreateFlags InstanceCreateFlags Bool := ⟨(·.v &&& ·.v != 0)⟩
instance : Inhabited InstanceCreateFlags := ⟨⟨0⟩⟩
structure ApplicationInfo where
  applicationName : String

kuruczgy

1. Set up WinDbg for kernel debugging, see this article: https://konradybcio.pl/windbg/
2. Download DebugView, extract it and start Dbgview64a.exe as administrator.
3. In the menu, enable Capture > Capture Kernel. Make sure Options > Force Carriage Returns is turned off, as this messes up the output. (You might want to also turn off the Capture > Capture (Global) Win32 options, they seem to make DebugView crash more often.)
4. In WinDgb, type the following commands:

   !amli dns x
   !amli set traceon
   !amli set spewon

The !amli dns x is just a bogus command and will fail, but it seems to be required to load the ACPI Debugger, and without it the subsequent commands will fail.

kuruczgy

def Sequence α n := (j : Nat) → j < n → α
def Sequence.map (f : α → β) (s : Sequence α n) : Sequence β n := fun j hj => f (s j hj)
instance : GetElem (Sequence α n) Nat α fun _ j => j < n where
  getElem s j hj := s j hj

structure NMealy (I O : Type) where
  S : Type
  S₀ : S → Prop
  Δ : S → I → O → S → Prop