--------------------
-- Slides
--------------------

data Term =
    Nat Integer
    | Abs String Term   -- EAbs Abstraction
    | Inv Term Term     -- EApp Invocation (a.k.a. Application) of a function
    | Var String        -- EVar a variable
    | Add

pretty x = case x of
    (Abs name term) -> "L" ++ name ++ "." ++ pretty term
    (Inv func param) -> "(" ++ pretty func ++ " " ++ pretty param ++ ")"
    (Var name) -> name
    Add -> "Add"

-- example
-- >>> pretty (Abs "x" $ Abs "y" $ Inv (Inv Add (Var "x")) (Var "y"))
-- "Lx.Ly.((Add x) y)"

--------------------
-- Exercise 1
--------------------
-- Ja
-- Nein
-- Ja
-- Nein

--------------------
-- Exercise 2
--------------------
-- ((Lx.(x z)) (Ly.(x y)))
-- ((Lx.(x z)) (Ly.(w (Lw.(((w y) z) x)))))
-- (Lx.((x y) (Lx.(y x))))

--------------------
-- Exercise 3
--------------------
-- (Lx.((x *z*) (Ly.(x y))))
-- ((Lx.(x *z*)) Ly.(*w* (Lw.(((w y) *z*) *x*))))
-- Lx.((x "y") (Lx.("y" x)))