gistfile1.txt

module Memory where

open import Data.Integer hiding (_+_ ; _*_ ; _≟_)
open import Data.Nat
open import Data.Maybe
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

mem = ℕ -> Maybe ℤ

empty : mem
empty x = nothing

write : ℕ -> ℤ -> mem -> mem
write i v m x with i ≟ x
...           | yes p = just v
...           | no ¬p = m x

lookup : ℕ -> mem -> Maybe ℤ
lookup i m = m i

hide : ℕ -> mem -> mem
hide i m x with i ≟ x
...        | yes p = nothing
...        | no ¬p = m x

write_eq : ∀ {i : ℕ}{v : ℤ}{m : mem} -> write i v m i ≡ just v
write_eq {i} with i ≟ i
write_eq | yes p = refl
write_eq | no ¬p = {!!}