
-- tripplemagic : Int -> Int -> Int -> Int;
-- tripplemagic x y z = ((\x:Int. x+x) x) + y + z;
-- main : Int;
-- main = tripplemagic ((\x:Int. x+x+3) ((\x:Int. x) 2)) 5 3
-- answer: 22

-- apply : (Int -> Int) -> Int -> Int;
-- apply f x = f x;
-- main : Int;
-- main = apply (\x : Int . x + 5) 5
-- answer: 10

-- apply : (Int -> Int -> Int) -> Int -> Int -> Int;
-- apply f x y = f x y;
-- krimp: Int -> Int -> Int;
-- krimp x y = x + y;
-- main : Int;
-- main = apply (krimp) 2 3;
-- answer: 5

-- fibbonaci : Int -> Int;
-- fibbonaci x = case x of {
--     0 => 0,
--     1 => 1,
--     -- abusing overflows to represent negatives like a boss
--     _ =>   (fibbonaci (x - 2))
--          + (fibbonaci (x - 1))
-- } : Int;
-- main : Int;
-- main = fibbonaci 10;
-- answer: 55

-- succ : Int -> Int;
-- succ x = x - 1;
-- 
-- isZero : Int -> Int;
-- isZero x = case x of {
--     0 => 1,
--     _ => 0
-- } : Int;
-- 
-- minimization : (Int -> Int) -> Int -> Int;
-- minimization p x = case p x of { 
--     1 => 0,
--     _ => minimization p (succ x)
-- } : Int;
-- 
-- main : Int;
-- main = minimization isZero 10;
-- answer: 0

posMul : Int -> Int -> Int;
posMul a b = case b of {
    0 => 0,
    _ => a + posMul a (b - 1)
} : Int;

facc : Int -> Int;
facc a = case a of {
    1 => 1,
    _ => posMul a (facc (a - 1))
} : Int;
-- main : Int;
-- main = facc 5
-- answer: 120

-- pow : Int -> Int -> Int;
-- pow a b = case b of {
--     0 => 1,
--     _ => posMul a (pow a (b-1))
-- } : Int;

minimization : (Int -> Int) -> Int -> Int;
minimization p x = case p x of { 
    1 => x,
    _ => minimization p (x + 1)
} : Int;

checkFac : Int -> Int;
checkFac x = case facc x of {
    0 => 1,
    _ => 0
} : Int;

main : Int;
main = minimization checkFac 1