tmp.tys

# enum List['T] = Nil
#      	      | Cons 'T List['T]

# enum Option['T] = None
#      	        | Some 'T

# def optMap : forall 'T 'U.Option['T] -> ('T -> 'U) -> Option['U]
#     	   = λo f.Option o None (λt.Some (f t))
# def optBind : forall 'T 'U.Option['T] -> ('T -> Option['U]) -> Option['U]
#     	    = λo f.Option o None (λt.f t)

# def hd : forall 'T. List['T] -> Option['T]
#        = λl. List l None (λh _.Some h)
# def tl : forall 'T. List['T] -> Option[List['T]]
#        = λl. List l None (λ_ t.Some t)
# def length : forall 'T. List['T] -> Integer
#     	   = λl. List l 0 (λ_ t.1 + (length t))
# def map : forall 'T 'U. List['T] -> ('T -> 'U) -> List['U]
#     	= λl f. List l Nil (λh t.Cons (f h) (map t f))

# def id    : forall 'a.'a -> 'a = λx.x
# def const : forall 'a.'a -> 'a -> 'a = λx y.x

# def foo : Integer -> Boolean = λx. if x == 0 then false else true

# def fact : Integer -> Integer
#     	 = λn.if n == 0 then 1 else n * fact (n - 1)

# def list : List[Integer] = (Cons 0 (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)))))
#def main : _ = map list fact

# def baz : (Integer, Boolean) -> Integer = \x. x.0
# def bar : (Integer, Boolean) = (baz (0, true), false)

# def main : _ = bar

# def main : Integer -> Integer -> List[Integer] -> List[Integer]
#     	 = \a b xs.let foo = \x.x + ((\_. a + b) ()) in
# 	      	   map xs foo
# def main : Boolean -> Integer -> Integer = \x y.(if x then 5 + 6 + 7 + y else 0) + 1


# def f : (forall 'a. 'a -> ('a, Integer)) -> Integer
#       = \x.(g 42).0
# def g : forall 'a. 'a -> ('a, Integer)
#       = \x.(x, f g)

#def main : Integer -> () -> () -> () -> () = \_ _ _ x.x
#def main : Integer -> Integer = \x.1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10 + x
#def main : Boolean -> Integer = \x.(if x then 1 + 1 else 1 * 2)
#def main : Boolean -> () = \x.if x then () else ()
#def main : Boolean -> Integer -> Integer -> Integer = \x y z.(if x then y+1 else z+1)
#def main : Integer -> Integer = λn.if n == 0 then 1 else n * main (n - 1)
def main : _ =
    λn. let rec go =
    	    λn acc.if n == 1
	       	   then acc
		   else go (n - 1) (acc * n)
	in go n 1
# def main : _ =
#     λn. let rec go =
#             λn acc.go n acc
# 	in go n n
# def main : Integer -> Integer = λn. let f = (\y.n + y) in f n

#def main : Boolean -> Integer -> Integer = \x y.1 + (if x then y else 4) + 5
#def main : Boolean -> Boolean -> Boolean = \x y. x && y
# def infrec : Boolean -> Boolean = \x.infrec x
# def main : Boolean = false && infrec true
#def foo : _ = 0
#def fact : Integer -> Integer = λn.if n == 0 then 1 else n * fact (n - 1)
#def main : _ = (\x y.(if x then (\z.z + y + 5) else (\z.z)) (fact 5) + 1) true 0

# def foo : forall 'T 'U. List['T] -> ('T -> 'U) -> List['U]
#     	= λl f. match l with
# 	        | Nil -> Nil
# 	        | Cons h t -> Cons (f h) (foo t)
# 	        end