module HomeworkEight
%default total
%access public export

data Exp = Var String | Abs String Exp | App Exp Exp

data Occur : List String -> Exp -> Type where
  OVar : Occur [s] (Var s)
  OAbs : Occur xs e -> Occur xs (Abs s e)
  OApp : Occur xs e1 -> Occur ys e2 -> Occur (xs ++ ys) (App e1 e2)

occ1 : Occur ["x"] (Var "x")
occ1 = OVar

occ2 : Occur ["x"] (Abs "y" (Var "x"))
occ2 = OAbs OVar

occ3 : Occur ["x","x"] (App (Var "x") (Var "x"))
occ3 = OApp OVar OVar

occ4 : Occur ["x","x"] (Abs "x" (App (Var "x") (Var "x")))
occ4 = OAbs occ3

--
-- -----------------
--    [x] @ x
--
--      xs @ e
-- -----------------
--    xs @ \x . e
--
--  xs @ e1  ys @ e2  zs = xs ++ ys
--  -------------------------------
--          zs @ e1 e2