Alfa proofs (or lack thereof)
Computing the memory address for given screen coordinates:
charAddr ∈ Column → Row → ScreenAddr charAddr (x,xr) (y,yr) = (lo screen + 2*(80*x+y),
A lemma for
All x,y . InRange xRange x ⇒ InRange yRange y ⇒ InRange screen (lo screen + 2*(80*x+y))
Decidable, should prove itself:
Formulate it as an expression of type
. The proof that a boolean is
the interpreter in Agda seems to be
to handle this...
Others have worked on this problem .