24 lines
514 B
Idris
24 lines
514 B
Idris
module HomeworkNine
|
|
import HomeworkEight
|
|
%default total
|
|
|
|
remove : Eq a => a -> List a -> List a
|
|
remove x = filter (/=x)
|
|
|
|
data FV : List String -> Exp -> Type where
|
|
FVar : FV [s] (Var s)
|
|
FAbs : FV xs e -> FV (remove s xs) (Abs s e)
|
|
FApp : FV xs e1 -> FV ys e2 -> FV (xs ++ ys) (App e1 e2)
|
|
|
|
fv1 : FV ["x"] (Var "x")
|
|
fv1 = FVar
|
|
|
|
fv2 : FV ["x"] (Abs "y" (Var "x"))
|
|
fv2 = FAbs FVar
|
|
|
|
fv3 : FV ["x","x"] (App (Var "x") (Var "x"))
|
|
fv3 = FApp FVar FVar
|
|
|
|
fv4 : FV [] (Abs "x" (App (Var "x") (Var "x")))
|
|
fv4 = FAbs fv3
|