GLFW Type Definitions

Opaque types for GLFW resources. Resources are managed via Lean External objects with automatic cleanup by finalizers on the C++ side.

opaque Hesper.GLFW.Window : Type

Opaque window handle with automatic cleanup via External finalizer

opaque Hesper.GLFW.Surface : Type

Opaque surface handle with automatic cleanup via External finalizer

opaque Hesper.GLFW.Texture : Type

Opaque texture handle with automatic cleanup via External finalizer

opaque Hesper.GLFW.TextureView : Type

Opaque texture view handle with automatic cleanup via External finalizer

opaque Hesper.GLFW.CommandEncoder : Type

Opaque command encoder handle with automatic cleanup via External finalizer

opaque Hesper.GLFW.RenderPassEncoder : Type

Opaque render pass encoder handle with automatic cleanup via External finalizer

opaque Hesper.GLFW.CommandBuffer : Type

Opaque command buffer handle with automatic cleanup via External finalizer

opaque Hesper.GLFW.ShaderModule : Type

Opaque shader module handle with automatic cleanup via External finalizer

opaque Hesper.GLFW.RenderPipeline : Type

Opaque render pipeline handle with automatic cleanup via External finalizer

inductive Hesper.GLFW.Key : Type

GLFW key codes

• escape : Key
• w : Key
• a : Key
• s : Key
• d : Key
• space : Key
• enter : Key
• other (code : Nat) : Key

def Hesper.GLFW.instInhabitedKey.default : Key

Equations

• Hesper.GLFW.instInhabitedKey.default = Hesper.GLFW.Key.escape

instance Hesper.GLFW.instInhabitedKey : Inhabited Key

Equations

• Hesper.GLFW.instInhabitedKey = { default := Hesper.GLFW.instInhabitedKey.default }

instance Hesper.GLFW.instReprKey : Repr Key

Equations

• Hesper.GLFW.instReprKey = { reprPrec := Hesper.GLFW.instReprKey.repr }

def Hesper.GLFW.instReprKey.repr : Key → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Hesper.GLFW.instReprKey.repr Hesper.GLFW.Key.escape prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GLFW.Key.escape")).group prec✝
• Hesper.GLFW.instReprKey.repr Hesper.GLFW.Key.w prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GLFW.Key.w")).group prec✝
• Hesper.GLFW.instReprKey.repr Hesper.GLFW.Key.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GLFW.Key.a")).group prec✝
• Hesper.GLFW.instReprKey.repr Hesper.GLFW.Key.s prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GLFW.Key.s")).group prec✝
• Hesper.GLFW.instReprKey.repr Hesper.GLFW.Key.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GLFW.Key.d")).group prec✝
• Hesper.GLFW.instReprKey.repr Hesper.GLFW.Key.space prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GLFW.Key.space")).group prec✝
• Hesper.GLFW.instReprKey.repr Hesper.GLFW.Key.enter prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GLFW.Key.enter")).group prec✝

def Hesper.GLFW.Key.toNat : Key → Nat

Equations

• Hesper.GLFW.Key.escape.toNat = 256
• Hesper.GLFW.Key.w.toNat = 87
• Hesper.GLFW.Key.a.toNat = 65
• Hesper.GLFW.Key.s.toNat = 83
• Hesper.GLFW.Key.d.toNat = 68
• Hesper.GLFW.Key.space.toNat = 32
• Hesper.GLFW.Key.enter.toNat = 257
• (Hesper.GLFW.Key.other a).toNat = a

inductive Hesper.GLFW.KeyAction : Type

Key action states

• release : KeyAction
• press : KeyAction
• repeated : KeyAction

def Hesper.GLFW.instInhabitedKeyAction.default : KeyAction

Equations

• Hesper.GLFW.instInhabitedKeyAction.default = Hesper.GLFW.KeyAction.release

instance Hesper.GLFW.instInhabitedKeyAction : Inhabited KeyAction

Equations

• Hesper.GLFW.instInhabitedKeyAction = { default := Hesper.GLFW.instInhabitedKeyAction.default }

def Hesper.GLFW.instReprKeyAction.repr : KeyAction → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Hesper.GLFW.instReprKeyAction : Repr KeyAction

Equations

• Hesper.GLFW.instReprKeyAction = { reprPrec := Hesper.GLFW.instReprKeyAction.repr }

def Hesper.GLFW.instBEqKeyAction.beq : KeyAction → KeyAction → Bool

Equations

• Hesper.GLFW.instBEqKeyAction.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Hesper.GLFW.instBEqKeyAction : BEq KeyAction

Equations

• Hesper.GLFW.instBEqKeyAction = { beq := Hesper.GLFW.instBEqKeyAction.beq }

def Hesper.GLFW.KeyAction.fromNat : Nat → KeyAction

Equations

• Hesper.GLFW.KeyAction.fromNat 0 = Hesper.GLFW.KeyAction.release
• Hesper.GLFW.KeyAction.fromNat 1 = Hesper.GLFW.KeyAction.press
• Hesper.GLFW.KeyAction.fromNat 2 = Hesper.GLFW.KeyAction.repeated
• Hesper.GLFW.KeyAction.fromNat x✝ = Hesper.GLFW.KeyAction.release