module InterpE data Expr = Var String      -- variables          | Val Int         -- values          | Add Expr Expr   -- addition data Eval : Type -> Type where     MkEval : (List (String, Int) -> Maybe a) -> Eval a fetch : String -> Eval Intfetch x = MkEval (\e => fetchVal e) where    fetchVal : List (String, Int) -> Maybe Int    fetchVal [] = Nothing    fetchVal ((v, val) :: xs) = if (x == v)                                  then (Just val)                                  else (fetchVal xs) Functor Eval where    map f (MkEval g) = MkEval (\e => map f (g e)) Applicative Eval where    pure x = MkEval (\e => Just x)     (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where        app : Maybe (a -> b) -> Maybe a -> Maybe b        app (Just fx) (Just gx) = Just (fx gx)        app _         _         = Nothing eval : Expr -> Eval Inteval (Var x)   = fetch xeval (Val x)   = [| x |]eval (Add x y) = [| eval x + eval y |] runEval : List (String, Int) -> Expr -> Maybe IntrunEval env e = case eval e of    MkEval envFn => envFn env