diff --git a/example.kind2 b/example.kind2
index 03dc1400..a717b729 100644
--- a/example.kind2
+++ b/example.kind2
@@ -27,12 +27,27 @@ Negate (xs: {List Bool}) : {List Bool} {
   Negate {Nil Bool}       = {Nil Bool}
 }
 
+Double (x: Nat) : Nat {
+  Double {Succ x} = {Succ {Succ (Double x)}}
+  Double {Zero}   = {Zero}
+}
+
+// FIXME: this won't check since `a != t`
 Tail (a: Type) (xs: {List a}) : {List a} {
   Tail a {Cons t x xs} = xs
 }
 
-Main (x: Bool) (y: {List Bool}) : Bool {
-  Main True  {Cons t x xs} = (And True Type)
-  Main False {Nil t}       = (And True Zero)
-}
+The (x: Nat) : Type
+Val (x: Nat) : {The x}
+
+Main : {The {Succ {Succ Zero}}} =
+  {Val (Double {Succ Zero})}
+
+
+
+
+
+
+
+
 
diff --git a/src/checker.hvm b/src/checker.hvm
index 2e33a2cc..76c4ee87 100644
--- a/src/checker.hvm
+++ b/src/checker.hvm
@@ -1,12 +1,12 @@
-//(Main n) =
-  //(Api.check_functions Functions)
-
-Main =
+Api.check_all =
   let output = (Api.output (Api.check_functions Functions))
   (Bool.if (String.is_empty output)
     "All terms check."
     output)
 
+Api.run_main =
+  (Show (Quote (Eval (Fn0 Main.)) 0) 0)
+
 (Api.check_functions Nil) = Nil
 (Api.check_functions (Cons f fs)) =
   let head = (Result f (Api.check_function f))
@@ -429,7 +429,7 @@ Main =
   // Checks others
   (Check term type) =
     ask term_typ = (Checker.bind (Infer term))
-    ask is_equal = (Checker.bind (Equal term_typ type))
+    ask is_equal = (Checker.bind (Equal (Eval term_typ) (Eval type)))
     (Bool.if is_equal
       // then
       (Checker.done Unit)
@@ -570,6 +570,10 @@ Main =
   (Eval (Var index)) =
     (Var index)
 
+  // Eval Inp
+  (Eval (Inp index)) =
+    (Var index)
+
   // Eval Typ
   (Eval Typ) =
     Typ
diff --git a/src/main.rs b/src/main.rs
index d52da807..03e7b434 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -10,26 +10,35 @@ fn main() -> Result<(), String> {
 
   let args: Vec<String> = std::env::args().collect();
 
-  if args.len() <= 2 || args[1] != "check" {
-    println!("{:?}", args);
-    println!("Usage: kind2 check file.kind");
+  if args.len() <= 2 || args[1] != "check" && args[1] != "run" {
+    println!("Usage:");
+    println!("$ kind2 check file.kind");
+    println!("$ kind2 run file.kind");
     return Ok(());
   }
 
   let path = &args[2];
   let file = match std::fs::read_to_string(path) {
-    Ok(code) => read_file(&code)?,
-    Err(msg) => read_file(&DEMO_CODE)?,
+    Ok(code) => read_file(&code),
+    Err(msg) => read_file(&DEMO_CODE),
   };
+  let file = match file {
+    Ok(file) => file,
+    Err(msg) => {
+      println!("{}", msg);
+      return Ok(());
+    }
+  };
+
   let code = compile_file(&file);
 
   let mut checker = (&CHECKER_HVM[0 .. CHECKER_HVM.find("////INJECT////").unwrap()]).to_string(); 
   checker.push_str(&code);
 
-  //std::fs::write("check.tmp.hvm", checker.clone()).ok(); writes checker to the checker.hvm file
+  std::fs::write("tmp.hvm", checker.clone()).ok(); // writes checker to the checker.hvm file
 
   let mut rt = hvm::Runtime::from_code(&checker)?;
-  let main = rt.alloc_code("Main")?;
+  let main = rt.alloc_code(if args[1] == "check" { "Api.check_all" } else { "Api.run_main" })?;
   rt.normalize(main);
   println!("{}", readback_string(&rt, main)); // TODO: optimize by deserializing term into text directly
 
@@ -430,7 +439,7 @@ pub fn compile_entry(entry: &Entry) -> String {
     let body = compile_term(&rule.body);
     let mut text = String::new();
     //text.push_str(&format!("    (Rule{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), body));
-    text.push_str(&format!("    (Rule{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), body));
+    text.push_str(&format!("    (Rule_{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), body));
     return text;
   }
 
@@ -442,7 +451,7 @@ pub fn compile_entry(entry: &Entry) -> String {
       let tail = compile_rule_chk(rule, index + 1, vars, args);
       return format!("(LHS {} {})", head, tail);
     } else {
-      return format!("(RHS (Rule{} {}.{}))", index, rule.name, args.iter().map(|x| format!(" {}", x)).collect::<Vec<String>>().join(""));
+      return format!("(RHS (Rule_{} {}.{}))", index, rule.name, args.iter().map(|x| format!(" {}", x)).collect::<Vec<String>>().join(""));
     }
   }
 
@@ -566,5 +575,5 @@ const DEMO_CODE: &str = "
     Tail a {Cons t x xs} = xs
   }
 
-  Main (x: Bool) (y: Nat) : {List Bool} = (Tail Bool {Cons Bool x {Cons Bool y {Nil Bool}}})
+  Main : {List Bool} = (Tail Bool {Cons Bool True {Cons Bool False {Nil Bool}}})
 ";