Text screen buffer access (2)
Using Predicate Based Subtyping
Let
Σ T P
denote the subset of type T that satisfies P
values are pairs: (value
x
∈T,proof of P
x
)
We can now define
type ScreenAddr = Σ Addr (InRange screen) screenPoke ∈ ScreenAddr → Word16 → H ()