This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |