diff --git a/Cargo.lock b/Cargo.lock
index 94a30715..bb318c06 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -101,12 +101,19 @@ dependencies = [
 ]
 
 [[package]]
-name = "hvm"
-version = "0.1.38"
+name = "highlight_error"
+version = "0.1.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f1e25cb7dd4f63d4640709b13cc1f330189e2195318eaf3ab372d732d12df3aa"
+checksum = "809e18805660d7b6b2e2b9f316a5099521b5998d5cba4dda11b5157a21aaef03"
+
+[[package]]
+name = "hvm"
+version = "0.1.40"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8f73a95e6ba27736390f1cdebea112de3740beebac40102291dc09917bd7e721"
 dependencies = [
  "clap",
+ "highlight_error",
  "itertools",
  "num_cpus",
  "regex",
diff --git a/Cargo.toml b/Cargo.toml
index 980128a0..f0851fc5 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -6,4 +6,4 @@ edition = "2021"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-hvm = "0.1.38"
+hvm = "0.1.40"
diff --git a/bench/nat_exp.kind2 b/bench/nat_exp.kind2
index b3d05b3e..626cfa6b 100644
--- a/bench/nat_exp.kind2
+++ b/bench/nat_exp.kind2
@@ -1,29 +1,26 @@
 Nat : Type
-  Z             : Nat
-  S (pred: Nat) : Nat
+Z : Nat
+S (pred: Nat) : Nat
 
 The (x: Nat) : Type
-  Val (x: Nat) : {The x}
+Val (x: Nat) : (The x)
 
-Add (a: Nat) (b: Nat) : Nat {
-  Add a {S b} = {S (Add a b)}
-  Add a {Z}   = a
+Add (a: Nat) (b: Nat) : Nat
+Add a (S b) = (S (Add a b))
+Add a (Z)   = a
+
+Mul (a: Nat) (b: Nat) : Nat
+Mul a (S b) = (Add a (Mul a b))
+Mul a (Z)   = (Z)
+
+Exp (a: Nat) (b: Nat) : Nat
+Exp a (S b) = (Mul a (Exp a b))
+Exp a (Z)   = (S Z)
+
+Nul (n: Nat) : Nat
+Nul (S a) = (Nul a)
+Nul (Z)   = (Z)
+
+Work : (The (Nul (Exp (S (S (S Z))) (S (S (S (S (S (S (S (S Z))))))))))) {
+  (Val Z)
 }
-
-Mul (a: Nat) (b: Nat) : Nat {
-  Mul a {S b} = (Add a (Mul a b))
-  Mul a {Z}   = {Z}
-}
-
-Exp (a: Nat) (b: Nat) : Nat {
-  Exp a {S b} = (Mul a (Exp a b))
-  Exp a {Z}   = {S Z}
-}
-
-Nul (n: Nat) : Nat {
-  Nul {S a}     = (Nul a)
-  Nul {Z}       = {Z}
-}
-
-Work : {The (Nul (Exp {S {S {S Z}}} {S {S {S {S {S {S {S {S Z}}}}}}}}))} =
-  {Val Z}
diff --git a/example.kind2 b/example.kind2
deleted file mode 100644
index dfa59612..00000000
--- a/example.kind2
+++ /dev/null
@@ -1,48 +0,0 @@
-Bool : Type
-  True  : Bool
-  False : Bool
-
-Nat : Type
-  Zero             : Nat
-  Succ (pred: Nat) : Nat
-
-List (a: Type) : Type
-  Nil  (a: Type)                       : {List a}
-  Cons (a: Type) (x: a) (xs: {List a}) : {List a}
-
-Not (a: Bool) : Bool {
-  Not True  = False
-  Not False = True
-}
-
-And (a: Bool) (b: Bool) : Bool {
-  And True  True  = True
-  And True  False = False
-  And False True  = False
-  And False False = False
-}
-
-Negate (xs: {List Bool}) : {List Bool} {
-  Negate {Cons Bool x xs} = {Cons Bool (Not x) (Negate xs)}
-  Negate {Nil Bool}       = {Nil Bool}
-}
-
-Double (x: Nat) : Nat {
-  Double {Succ x} = {Succ {Succ (Double x)}}
-  Double {Zero}   = {Zero}
-}
-
-// FIXME: shouldn't type-check, but does due to Inp treatment
-Tail (a: Type) (xs: {List a}) : {List a} {
-  Tail a {Cons t x xs} = x
-}
-  
-Main : Nat = (Double {Succ {Succ Zero}})
-
-
-
-
-
-
-
-
diff --git a/src/main.rs b/src/main.rs
index f3ad291c..bcb3f86f 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,13 +1,15 @@
 #![allow(dead_code)] 
 #![allow(unused_variables)] 
 
-// TODO: type{} syntax
+mod language;
 
-use std::collections::HashMap;
+use language::{*};
 use hvm::parser as parser;
 
+const CHECKER_HVM: &str = include_str!("checker.hvm");
+
 fn main() -> Result<(), String> {
-  gen();
+  //gen_debug_file();
 
   let args: Vec<String> = std::env::args().collect();
 
@@ -19,10 +21,17 @@ fn main() -> Result<(), String> {
   }
 
   let path = &args[2];
+
+  // Reads definitions from file
   let file = match std::fs::read_to_string(path) {
     Ok(code) => read_file(&code),
-    Err(msg) => read_file(&DEMO_CODE),
+    Err(msg) => {
+      println!("File not found: {}", path);
+      return Ok(());
+    },
   };
+
+  // Prints errors if parsing failed
   let file = match file {
     Ok(file) => file,
     Err(msg) => {
@@ -31,569 +40,68 @@ fn main() -> Result<(), String> {
     }
   };
 
-  let code = compile_file(&file);
+  // Adjusts the file
+  let file = adjust_file(&file);
 
+  //for (name, entry) in &file.entries {
+    //println!("[{}]\n{}\n", name, show_entry(entry));
+  //}
+
+  // 
+  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(format!("{}.hvm", path), checker.clone()).ok(); // writes checker to the checker.hvm file
+  // Writes the checker file.kind2.hvm
+  std::fs::write(format!("{}.hvm", path), checker.clone()).ok();
 
+  // Runs with the interpreter 
   let mut rt = hvm::Runtime::from_code(&checker)?;
   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
 
+  // Display stats
   println!("Rewrites: {}", rt.get_rewrites());
 
   return Ok(());
 }
 
-fn gen() {
-  let file = read_file(&DEMO_CODE).unwrap();
+// ------------------------------------------------------------
+// ------------------------------------------------------------
+// ------------------------------------------------------------
+
+fn debug_print_parser_state(txt: &str, state: &parser::State) {
+  println!("{} ||{}", txt, &state.code[state.index..state.index+32].replace("\n"," || "));
+}
+
+fn gen_debug_file() {
+  let file = match read_file(&DEBUG_CODE) {
+    Ok(file) => file,
+    Err(msg) => {
+      println!("{}", msg);
+      return;
+    }
+  };
   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("tmp.hvm", checker.clone()).ok(); // writes checker to the checker.hvm file
+  std::fs::write("debug.hvm", checker.clone()).ok(); // writes checker to the checker.hvm file
 }
 
-const CHECKER_HVM: &str = include_str!("checker.hvm");
+const DEBUG_CODE: &str = "
+Bool : Type
+True : Bool
+False : Bool
 
-#[derive(Clone, Debug)]
-pub enum Term {
-  Typ,
-  Var { name: String },
-  Let { name: String, expr: Box<Term>, body: Box<Term> },
-  All { name: String, tipo: Box<Term>, body: Box<Term> },
-  Lam { name: String, body: Box<Term> },
-  App { func: Box<Term>, argm: Box<Term> },
-  Ctr { name: String, args: Vec<Box<Term>> },
-  Fun { name: String, args: Vec<Box<Term>> },
-}
-
-#[derive(Clone, Debug)]
-pub struct Argument {
-  eras: bool,
-  name: String,
-  tipo: Box<Term>,
-}
-
-#[derive(Clone, Debug)]
-pub struct Rule {
-  name: String,
-  pats: Vec<Box<Term>>,
-  body: Box<Term>,
-}
-
-#[derive(Clone, Debug)]
-pub struct Entry {
-  name: String,
-  args: Vec<Box<Argument>>,
-  tipo: Box<Term>,
-  rules: Vec<Box<Rule>>
-}
-
-#[derive(Clone, Debug)]
-pub struct File {
-  entries: HashMap<String, Box<Entry>>
-}
-
-// Parser
-// ======
-
-pub fn parse_var(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
-  parser::guard(
-    Box::new(|state| {
-      let (state, head) = parser::get_char(state)?;
-      Ok((state, ('a'..='z').contains(&head) || head == '_' || head == '$'))
-    }),
-    Box::new(|state| {
-      let (state, name) = parser::name(state)?;
-      Ok((state, Box::new(Term::Var { name })))
-    }),
-    state,
-  )
-}
-
-pub fn parse_lam(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
-  parser::guard(
-    parser::text_parser("@"),
-    Box::new(move |state| {
-      let (state, _)    = parser::consume("@", state)?;
-      let (state, name) = parser::name(state)?;
-      let (state, body) = parse_term(state)?;
-      Ok((state, Box::new(Term::Lam { name, body })))
-    }),
-    state,
-  )
-}
-
-pub fn parse_all(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
-  parser::guard(
-    Box::new(|state| {
-      let (state, all0) = parser::text("(", state)?;
-      let (state, name) = parser::name(state)?;
-      let (state, all1) = parser::text(":", state)?;
-      Ok((state, all0 && all1 && name.len() > 0))
-    }),
-    Box::new(|state| {
-      let (state, _)    = parser::consume("(", state)?;
-      let (state, name) = parser::name(state)?;
-      let (state, _)    = parser::consume(":", state)?;
-      let (state, tipo) = parse_term(state)?;
-      let (state, _)    = parser::consume(")", state)?;
-      let (state, body) = parse_term(state)?;
-      Ok((state, Box::new(Term::All { name, tipo, body })))
-    }),
-    state,
-  )
-}
-
-pub fn parse_app(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
-  return parser::guard(
-    parser::text_parser("("),
-    Box::new(|state| {
-      parser::list(
-        parser::text_parser("("),
-        parser::text_parser(""),
-        parser::text_parser(")"),
-        Box::new(parse_term),
-        Box::new(|args| {
-          if !args.is_empty() {
-            args.into_iter().reduce(|a, b| Box::new(Term::App { func: a, argm: b })).unwrap()
-          } else {
-            Box::new(Term::Var { name: "?".to_string() })
-          }
-        }),
-        state,
-      )
-    }),
-    state,
-  );
-}
-
-pub fn parse_let(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
-  return parser::guard(
-    parser::text_parser("let "),
-    Box::new(|state| {
-      let (state, _)    = parser::consume("let ", state)?;
-      let (state, name) = parser::name1(state)?;
-      let (state, _)    = parser::consume("=", state)?;
-      let (state, expr) = parse_term(state)?;
-      let (state, _)    = parser::text(";", state)?;
-      let (state, body) = parse_term(state)?;
-      Ok((state, Box::new(Term::Let { name, expr, body })))
-    }),
-    state,
-  );
-}
-
-pub fn parse_ctr(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
-  parser::guard(
-    Box::new(|state| {
-      let (state, _)    = parser::text("{", state)?;
-      let (state, head) = parser::get_char(state)?;
-      Ok((state, ('A'..='Z').contains(&head)))
-    }),
-    Box::new(|state| {
-      let (state, open) = parser::text("{", state)?;
-      let (state, name) = parser::name1(state)?;
-      if name == "Type" {
-        Ok((state, Box::new(Term::Typ)))
-      } else {
-        let (state, args) = if open {
-          parser::until(parser::text_parser("}"), Box::new(parse_term), state)?
-        } else {
-          (state, Vec::new())
-        };
-        Ok((state, Box::new(Term::Ctr { name, args })))
-      }
-    }),
-    state,
-  )
-}
-
-pub fn parse_fun(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
-  parser::guard(
-    Box::new(|state| {
-      let (state, _)    = parser::text("(", state)?;
-      let (state, head) = parser::get_char(state)?;
-      Ok((state, ('A'..='Z').contains(&head)))
-    }),
-    Box::new(|state| {
-      let (state, open) = parser::text("(", state)?;
-      let (state, name) = parser::name1(state)?;
-      let (state, args) = if open {
-        parser::until(parser::text_parser(")"), Box::new(parse_term), state)?
-      } else {
-        (state, Vec::new())
-      };
-      Ok((state, Box::new(Term::Fun { name, args })))
-    }),
-    state,
-  )
-}
-
-pub fn parse_term(state: parser::State) -> parser::Answer<Box<Term>> {
-  parser::grammar(
-    "Term",
-    &[
-      Box::new(parse_let), // `let `
-      Box::new(parse_all), // `(name:`
-      Box::new(parse_ctr), // `{Name`
-      Box::new(parse_fun), // `(Name`
-      Box::new(parse_app), // `(`
-      Box::new(parse_lam), // `@`
-      Box::new(parse_var), // 
-      Box::new(|state| Ok((state, None))),
-    ],
-    state,
-  )
-}
-
-pub fn parse_entry(state: parser::State) -> parser::Answer<Box<Entry>> {
-  let (state, name) = parser::name1(state)?;
-  let (state, args) = parser::until(parser::text_parser(":"), Box::new(parse_argument), state)?;
-  let (state, tipo) = parse_term(state)?;
-  let (state, head) = parser::peek_char(state)?;
-  if head == '=' {
-    let (state, _)    = parser::consume("=", state)?;
-    let (state, body) = parse_term(state)?;
-    let mut pats = vec![];
-    for arg in &args {
-      pats.push(Box::new(Term::Var { name: arg.name.clone() }));
-    }
-    let rules = vec![Box::new(Rule { name: name.clone(), pats, body })];
-    return Ok((state, Box::new(Entry { name, args, tipo, rules })));
-  } else if head == '{' {
-    let (state, _)    = parser::consume("{", state)?;
-    let name_clone = name.clone();
-    let (state, rules) = parser::until(parser::text_parser("}"), Box::new(move |state| parse_rule(state, name_clone.clone())), state)?;
-    return Ok((state, Box::new(Entry { name, args, tipo, rules })));
-  } else {
-    return Ok((state, Box::new(Entry { name, args, tipo, rules: vec![] })));
-  }
-}
-
-pub fn parse_rule(state: parser::State, name: String) -> parser::Answer<Box<Rule>> {
-  let (state, _)    = parser::consume(&name, state)?;
-  let (state, pats) = parser::until(parser::text_parser("="), Box::new(parse_term), state)?;
-  let (state, body) = parse_term(state)?;
-  return Ok((state, Box::new(Rule { name, pats, body })));
-}
-
-pub fn parse_argument(state: parser::State) -> parser::Answer<Box<Argument>> {
-  let (state, _)    = parser::consume("(", state)?;
-  let (state, name) = parser::name1(state)?;
-  let (state, _)    = parser::consume(":", state)?;
-  let (state, tipo) = parse_term(state)?;
-  let (state, _)    = parser::consume(")", state)?;
-  return Ok((state, Box::new(Argument { eras: false, name, tipo })));
-}
-
-pub fn parse_file(state: parser::State) -> parser::Answer<Box<File>> {
-  let (state, entry_vec) = parser::until(Box::new(parser::done), Box::new(parse_entry), state)?;
-  let mut entries = HashMap::new();
-  for entry in entry_vec {
-    entries.insert(entry.name.clone(), entry);
-  }
-  return Ok((state, Box::new(File { entries })));
-}
-
-pub fn show_term(term: &Term) -> String {
-  match term {
-    Term::Typ => {
-      format!("Type")
-    }
-    Term::Var { name } => {
-      format!("{}", name)
-    }
-    Term::Let { name, expr, body } => {
-      let expr = show_term(expr);
-      let body = show_term(body);
-      format!("let {} = {}; {}", name, expr, body)
-    }
-    Term::Lam { name, body } => {
-      let body = show_term(body);
-      format!("@{}({})", name, body)
-    }
-    Term::App { func, argm } => {
-      let mut args = vec![argm];
-      let mut expr = func;
-      while let Term::App { func, argm } = &**expr {
-        args.push(argm);
-        expr = func;
-      }
-      args.reverse();
-      format!("({} {})", show_term(expr), args.iter().map(|x| show_term(x)).collect::<Vec<String>>().join(" "))
-    }
-    Term::All { name, tipo, body } => {
-      let body = show_term(body);
-      format!("({}: {}) {}", name, show_term(tipo), body)
-    }
-    Term::Ctr { name, args } => {
-      format!("{{{}{}}}", name, args.iter().map(|x| format!(" {}",show_term(x))).collect::<String>())
-    }
-    Term::Fun { name, args } => {
-      format!("({}{})", name, args.iter().map(|x| format!(" {}",show_term(x))).collect::<String>())
-    }
-  }
-}
-
-pub fn show_rule(rule: &Rule) -> String {
-  let name = &rule.name;
-  let mut pats = vec![];
-  for pat in &rule.pats {
-    pats.push(show_term(pat));
-  }
-  let body = show_term(&rule.body);
-  format!("{} {} => {}", name, pats.join(" "), body)
-}
-
-pub fn show_entry(entry: &Entry) -> String {
-  let name = &entry.name;
-  let mut args = vec![];
-  for arg in &entry.args {
-    args.push(format!(" ({}: {})", arg.name, show_term(&arg.tipo)));
-  }
-  if entry.rules.len() == 0 {
-    format!("{}{} : {}", name, args.join(""), show_term(&entry.tipo))
-  } else {
-    let mut rules = vec![];
-    for rule in &entry.rules {
-      rules.push(format!("\n  {}", show_rule(rule)));
-    }
-    format!("{}{} : {} {{{}\n}}", name, args.join(""), show_term(&entry.tipo), rules.join(""))
-  }
-}
-
-pub fn show_file(file: &File) -> String {
-  let mut entries = vec![];
-  for entry in file.entries.values() {
-    entries.push(show_entry(entry));
-  }
-  entries.join("\n")
-}
-
-pub fn read_term(code: &str) -> Result<Box<Term>, String> {
-  parser::read(Box::new(parse_term), code)
-}
-
-pub fn read_file(code: &str) -> Result<Box<File>, String> {
-  parser::read(Box::new(parse_file), code)
-}
-
-// Compiler
-// ========
-
-//pub enum Term {
-  //Typ,
-  //Var { name: String },
-  //Let { name: String, expr: Box<Term>, body: Box<Term> },
-  //App { func: Box<Term>, argm: Box<Term> },
-  //Lam { name: String, body: Box<Term> },
-  //All { name: String, tipo: Box<Term>, body: Box<Term> },
-  //Ctr { name: String, args: Vec<Box<Term>> },
-  //Fun { name: String, args: Vec<Box<Term>> },
-//}
-pub fn compile_term(term: &Term, quote: bool) -> String { 
-  match term {
-    Term::Typ => {
-      format!("Typ")
-    }
-    Term::Var { name } => {
-      name.clone()
-    }
-    Term::Let { name, expr, body } => {
-      todo!()
-    }
-    Term::All { name, tipo, body } => {
-      format!("(All {} λ{} {})", compile_term(tipo, quote), name, compile_term(body, quote))
-    }
-    Term::Lam { name, body } => {
-      format!("(Lam λ{} {})", name, compile_term(body, quote))
-    }
-    Term::App { func, argm } => {
-      format!("({} {} {})", if quote { "App" } else { "Apply" }, compile_term(func, quote), compile_term(argm, quote))
-    }
-    Term::Ctr { name, args } => {
-      let mut args_strs : Vec<String> = Vec::new();
-      for arg in args {
-        args_strs.push(format!(" {}", compile_term(arg, quote)));
-      }
-      format!("(Ct{} {}.{})", args.len(), name, args_strs.join(""))
-    }
-    Term::Fun { name, args } => {
-      let mut args_strs : Vec<String> = Vec::new();
-      for arg in args {
-        args_strs.push(format!(" {}", compile_term(arg, quote)));
-      }
-      format!("({}{} {}.{})", if quote { "NewFn" } else { "Rule_" }, args.len(), name, args_strs.join(""))
-    }
-  }
-}
-
-pub fn compile_entry(entry: &Entry) -> String {
-  fn compile_type(args: &Vec<Box<Argument>>, tipo: &Box<Term>, index: usize) -> String {
-    if index < args.len() {
-      let arg = &args[index];
-      format!("(All {} λ{} {})", compile_term(&arg.tipo, false), arg.name, compile_type(args, tipo, index + 1))
-    } else {
-      compile_term(tipo, false)
-    }
-  }
-
-  fn compile_rule(rule: &Rule) -> String {
-    let mut pats = vec![];
-    for pat in &rule.pats {
-      pats.push(format!(" {}", compile_term(pat, false)));
-    }
-    let body_quot = compile_term(&rule.body, true);
-    let body_exec = compile_term(&rule.body, false);
-    let mut text = String::new();
-    //text.push_str(&format!("    (Rule{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), body));
-    text.push_str(&format!("    (Body_{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), body_quot));
-    text.push_str(&format!("    (Rule_{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), body_exec));
-    return text;
-  }
-
-  fn compile_rule_chk(rule: &Rule, index: usize, vars: &mut u64, args: &mut Vec<String>) -> String {
-    if index < rule.pats.len() {
-      let (inp_patt_str, var_patt_str) = compile_patt_chk(&rule.pats[index], vars);
-      args.push(var_patt_str);
-      let head = inp_patt_str;
-      let tail = compile_rule_chk(rule, index + 1, vars, args);
-      return format!("(LHS {} {})", head, tail);
-    } else {
-      return format!("(RHS (Body_{} {}.{}))", index, rule.name, args.iter().map(|x| format!(" {}", x)).collect::<Vec<String>>().join(""));
-    }
-  }
-
-  fn compile_patt_chk(patt: &Term, vars: &mut u64) -> (String, String) {
-    match patt {
-      Term::Var { .. } => {
-        let inp = format!("(Inp {})", vars);
-        let var = format!("(Var {})", vars);
-        *vars += 1;
-        return (inp, var);
-      }
-      Term::Ctr { name, args } => {
-        let mut inp_args_str = String::new();
-        let mut var_args_str = String::new();
-        for arg in args {
-          let (inp_arg_str, var_arg_str) = compile_patt_chk(arg, vars);
-          inp_args_str.push_str(&format!(" {}", inp_arg_str));
-          var_args_str.push_str(&format!(" {}", var_arg_str));
-        }
-        let inp_str = format!("(Ct{} {}.{})", args.len(), name, inp_args_str);
-        let var_str = format!("(Ct{} {}.{})", args.len(), name, var_args_str);
-        return (inp_str, var_str);
-      }
-      _ => {
-        panic!("Invalid left-hand side pattern: {}", show_term(patt));
-      }
-    }
-  }
-
-  let mut result = String::new();
-  result.push_str(&format!("    (NameOf {}.) = \"{}\"\n", entry.name, entry.name));
-  result.push_str(&format!("    (HashOf {}.) = %{}\n", entry.name, entry.name));
-  result.push_str(&format!("    (TypeOf {}.) = {}\n", entry.name, compile_type(&entry.args, &entry.tipo, 0)));
-  for rule in &entry.rules {
-    result.push_str(&compile_rule(&rule));
-  }
-  result.push_str(&format!("    (Verify {}.) =\n", entry.name));
-  for rule in &entry.rules {
-    result.push_str(&format!("      (Cons {}\n", compile_rule_chk(&rule, 0, &mut 0, &mut vec![]))); 
-  }
-  result.push_str(&format!("      Nil{}\n", ")".repeat(entry.rules.len())));
-  return result;
-}
-
-pub fn compile_file(file: &File) -> String {
-  let mut result = String::new();
-  result.push_str(&format!("\n  Functions =\n"));
-  result.push_str(&format!("    let fns = Nil\n"));
-  for entry in file.entries.values() {
-    result.push_str(&format!("    let fns = (Cons {}. fns)\n", entry.    name));
-  }
-  result.push_str(&format!("    fns\n\n"));
-  for entry in file.entries.values() {
-    result.push_str(&format!("  // {}\n", entry.name));
-    result.push_str(&format!("  // {}\n", "-".repeat(entry.name.len())));
-    result.push_str(&format!("\n"));
-    result.push_str(&compile_entry(&entry));
-    result.push_str(&format!("\n"));
-  }
-  return result;
-}
-
-fn readback_string(rt: &hvm::Runtime, host: u64) -> String {
-  let str_cons = rt.get_id("String.cons");
-  let str_nil  = rt.get_id("String.nil");
-  let mut term = rt.ptr(host);
-  let mut text = String::new();
-  //let str_cons = rt.
-  loop {
-    if hvm::get_tag(term) == hvm::CTR {
-      let fid = hvm::get_ext(term);
-      if fid == str_cons {
-        let head = rt.ptr(hvm::get_loc(term, 0));
-        let tail = rt.ptr(hvm::get_loc(term, 1));
-        if hvm::get_tag(head) == hvm::NUM {
-          text.push(std::char::from_u32(hvm::get_num(head) as u32).unwrap_or('?'));
-          term = tail;
-          continue;
-        }
-      }
-      if fid == str_nil {
-        break;
-      }
-    }
-    panic!("Invalid output: {} {}", hvm::get_tag(term), rt.show(host));
-  }
-  return text;
-}
-
-const DEMO_CODE: &str = "
 Nat : Type
-  Zero             : Nat
-  Succ (pred: Nat) : Nat
+Zero : Nat
+Succ (pred: Nat) : Nat
 
-The (x: Nat) : Type
-  Val (x: Nat) : {The x}
+List (a: Type) : Type
+Nil  (a: Type) : (List a)
+Cons (a: Type) (x: a) (xs: (List a)) : (List a)
 
-Double (x: Nat) : Nat {
-  Double {Succ x} = {Succ {Succ (Double x)}}
-  Double {Zero}   = {Zero}
-}
-
-Pow2 (x: Nat) : Nat {
-  Pow2 {Succ x} = (Double (Pow2 x))
-  Pow2 {Zero}   = {Succ Zero}
-}
-
-Destroy (x: Nat) : Nat {
-  Destroy {Succ n} = (Destroy n)
-  Destroy {Zero}   = {Zero}
-}
-
-SlowNumber : Nat =
-  (Destroy (Pow2
-    {Succ {Succ {Succ {Succ
-    {Succ {Succ {Succ {Succ
-    {Succ {Succ {Succ {Succ
-    {Succ {Succ {Succ {Succ
-    {Succ {Succ {Succ {Succ
-    {Succ {Succ {Succ {Succ
-    Zero
-    }}}}
-    }}}}
-    }}}}
-    }}}}
-    }}}}
-    }}}}
-  ))
-  
-// Proof that SlowNumber is 0
-Main : {The (SlowNumber)} = {Val Zero}
+Not (a: Bool) : Bool
+Not True  = False
 ";