data Range = Range { lo,hi∈Addr }
screen ∈ Range
screen = Range 0xb8000 0xb8fff
InRange ∈ Range → Addr → Prop
screenPoke ∈ (a∈Addr) → InRange screen a → Word16 → H ()
Implementation of screenPoke
writableScreen ∈ (a∈Addr) → InRange screen a → Writable a
writableScreen a r = Unsafe.writable a
screenPoke ∈ (a∈Addr)→ InRange screen a → Word16 → H ()
screenPoke a r d = poke16 a (writableScreen a r) d