diff --git a/bin/miniFunPolyInterpreter.ml b/bin/miniFunPolyInterpreter.ml
index df42297..520586c 100644
--- a/bin/miniFunPolyInterpreter.ml
+++ b/bin/miniFunPolyInterpreter.ml
@@ -29,6 +29,14 @@ let () =
       ()
   in
 
+  let evalb = Clap.flag
+      ~description: "Optional flag for evaluating the generated risc code."
+      ~section: values
+      ~set_long: "eval"
+      ~set_short: 'e'
+      false
+  in
+
   let output = Clap.optional_string
       ~description: "Output file. If not specified output is printed on stdout."
       ~placeholder: "FILENAME"
@@ -63,26 +71,32 @@ let () =
         exit (-1)
     in
     let ty_program =
-      match TypeChecker.typecheck_polymorphic program with
+      match TypeChecker.typecheck_polymorphic_unbound program with
       | Ok ty -> ty
       | Error (`AbsentAssignment msg)
       | Error (`WrongTypeSpecification msg)
+      | Error (`RecusrionsNotImplemented msg)
       | Error (`WrongType msg) ->
         Printf.fprintf stderr "%s\n" msg;
         exit (-1)
     in
     let return_value =
-      match Semantics.reduce program inval with
-        Ok o -> o
-      | Error (`AbsentAssignment msg)
-      | Error (`DivisionByZero msg)
-      | Error (`WrongType msg) ->
-        Printf.fprintf stderr "%s\n" msg;
-        exit (-1)
+      if evalb then
+        match Semantics.reduce program inval with
+          Ok o -> Some o
+        | Error (`AbsentAssignment msg)
+        | Error (`DivisionByZero msg)
+        | Error (`WrongType msg) ->
+          Printf.fprintf stderr "%s\n" msg;
+          exit (-1)
+      else
+        None
     in
 
     Printf.fprintf outch "Type of the program: %s\n" (Types.pp_type_f ty_program);
-    Printf.fprintf outch "%d\n" return_value
+    match return_value with
+    | Some v -> Printf.fprintf outch "%d\n" v
+    | None -> ()
   in
 
 
diff --git a/bin/testing.minifun b/bin/testing.minifun
deleted file mode 100644
index 93973b2..0000000
--- a/bin/testing.minifun
+++ /dev/null
@@ -1,5 +0,0 @@
-\n: int =>
-let fn =
-    \x: int => x + n
-in
-fn n
diff --git a/lib/miniFun/TypeChecker.ml b/lib/miniFun/TypeChecker.ml
index aec5bf7..9fe72f7 100644
--- a/lib/miniFun/TypeChecker.ml
+++ b/lib/miniFun/TypeChecker.ml
@@ -251,7 +251,16 @@ let rec evaluate_type_polimorphic program (env: env) level =
     let* var_ty = evaluate_type_polimorphic xval env (level + 1) in
     let generalized_ty = generalize level var_ty in
     evaluate_type_polimorphic rest (VariableMap.add x generalized_ty env) level
-  | LetFun (_f, _xs, _typef, _fbody, _rest) -> failwith "Not Implemented"
+  | LetFun (f, xs, _typef, fbody, rest) ->
+    let* _ = Error (`RecusrionsNotImplemented "Let Rec is not implemented.") in
+    let tmp_type_f = VariableTypeP (ref (Unbound (new_global_id (), level))) in
+    let new_env = VariableMap.add f tmp_type_f env in
+    let param_type = VariableTypeP (ref (Unbound (new_global_id (), level))) in
+    let fn_env = VariableMap.add xs param_type new_env in
+    let* body_type = evaluate_type_polimorphic fbody fn_env level in
+    let* _ = unify tmp_type_f body_type in
+    evaluate_type_polimorphic rest (VariableMap.add f tmp_type_f env) level
+
 
 (* -------------------------------------------------------------------------- *)
 
@@ -419,3 +428,10 @@ let typecheck_polymorphic (program: t_exp)
   in
   let generalized_ty = generalize (-1) type_program in
   Ok (generalized_ty)
+
+let typecheck_polymorphic_unbound (program: t_exp)
+  : (type_f, [> typechecking_error]) result =
+  global_type_id := 0;
+  let* type_program = evaluate_type_polimorphic program VariableMap.empty 0 in
+  let generalized_ty = generalize (-1) type_program in
+  Ok (generalized_ty)
diff --git a/lib/miniFun/TypeChecker.mli b/lib/miniFun/TypeChecker.mli
index 3158bc9..e6148e7 100644
--- a/lib/miniFun/TypeChecker.mli
+++ b/lib/miniFun/TypeChecker.mli
@@ -1,3 +1,5 @@
-val typecheck : Types.t_exp -> (Types.ftype, [> Types.typechecking_error]) result
+val typecheck                     : Types.t_exp -> (Types.ftype,  [> Types.typechecking_error]) result
 
-val typecheck_polymorphic : Types.t_exp -> (Types.type_f, [> Types.typechecking_error]) result
+val typecheck_polymorphic         : Types.t_exp -> (Types.type_f, [> Types.typechecking_error]) result
+
+val typecheck_polymorphic_unbound : Types.t_exp -> (Types.type_f, [> Types.typechecking_error]) result
diff --git a/lib/miniFun/Types.ml b/lib/miniFun/Types.ml
index 883ea2e..f8f79da 100644
--- a/lib/miniFun/Types.ml
+++ b/lib/miniFun/Types.ml
@@ -134,6 +134,7 @@ type base_error = [
 type typechecking_error = [
   | base_error
   | `WrongTypeSpecification of string
+  | `RecusrionsNotImplemented of string
 ]
 
 type error = [
diff --git a/lib/miniFun/Types.mli b/lib/miniFun/Types.mli
index c3af3a6..374b6ca 100644
--- a/lib/miniFun/Types.mli
+++ b/lib/miniFun/Types.mli
@@ -29,20 +29,6 @@ module IntegerMap : Map.S with type key = int
 
 val pp_type_f : type_f -> string
 
-(* module VariableTypeMap : Map.S with type key = variable_type *)
-
-(* type substitution = (\* from variable types to politypes *\) *)
-(*   politype VariableTypeMap.t *)
-
-(* type prefix = *)
-(*   | Lambda *)
-(*   | Let *)
-(*   | LetRec *)
-
-(* type typed_prefix = *)
-(*   (\* list of free variables in the context and the associated type *\) *)
-(*   (prefix * politype) VariableMap.t *)
-
 (* -------------------------------------------------------------------------- *)
 
 type ftype = (* type used for specification *)
@@ -106,6 +92,7 @@ type base_error = [
 type typechecking_error = [
   | base_error
   | `WrongTypeSpecification of string
+  | `RecusrionsNotImplemented of string
 ]
 
 type error = [