35 lines
738 B
Idris
35 lines
738 B
Idris
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
|