diff --git a/book/Tests/CtrGen/ParamsTest.kind2 b/book/Tests/CtrGen/ParamsTest.kind2
new file mode 100644
index 0000000..98df41e
--- /dev/null
+++ b/book/Tests/CtrGen/ParamsTest.kind2
@@ -0,0 +1,3 @@
+data Tests/CtrGen/ParamsTest T Z
+| ctr1 : (Tests/CtrGen/ParamsTest T Z)
+| ctr2 : (Tests/CtrGen/ParamsTest T Z)
diff --git a/book/Tests/CtrGen/ParamsTest/ctr1.kind2 b/book/Tests/CtrGen/ParamsTest/ctr1.kind2
new file mode 100644
index 0000000..d663fcc
--- /dev/null
+++ b/book/Tests/CtrGen/ParamsTest/ctr1.kind2
@@ -0,0 +1,2 @@
+ctr1 <T> <Z> : (Tests/CtrGen/ParamsTest T Z) = 
+ ~λP λctr1 λctr2 (ctr1)
\ No newline at end of file
diff --git a/book/Tests/CtrGen/ParamsTest/ctr2.kind2 b/book/Tests/CtrGen/ParamsTest/ctr2.kind2
new file mode 100644
index 0000000..a755586
--- /dev/null
+++ b/book/Tests/CtrGen/ParamsTest/ctr2.kind2
@@ -0,0 +1,2 @@
+ctr2 <T> <Z> : (Tests/CtrGen/ParamsTest T Z) = 
+ ~λP λctr1 λctr2 (ctr2)
\ No newline at end of file
diff --git a/book/Tests/CtrGen/VectorTest.kind2 b/book/Tests/CtrGen/VectorTest.kind2
new file mode 100644
index 0000000..6533cfb
--- /dev/null
+++ b/book/Tests/CtrGen/VectorTest.kind2
@@ -0,0 +1,6 @@
+data Tests/CtrGen/VectorTest T (len: Nat)
+| cons (len: Nat)
+       (head: T)
+       (tail: (Tests/CtrGen/VectorTest T len)) :
+       (Tests/CtrGen/VectorTest T (Nat/succ len))
+| nil : (Tests/CtrGen/VectorTest T Nat/zero)
diff --git a/book/Tests/CtrGen/VectorTest/cons.kind2 b/book/Tests/CtrGen/VectorTest/cons.kind2
new file mode 100644
index 0000000..e07ca9f
--- /dev/null
+++ b/book/Tests/CtrGen/VectorTest/cons.kind2
@@ -0,0 +1,2 @@
+cons <T> (len: Nat) (head: T) (tail: (Tests/CtrGen/VectorTest T len)) : (Tests/CtrGen/VectorTest T (Nat/succ len)) = 
+ ~λP λcons λnil (cons len head tail)
\ No newline at end of file
diff --git a/book/Tests/CtrGen/VectorTest/nil.kind2 b/book/Tests/CtrGen/VectorTest/nil.kind2
new file mode 100644
index 0000000..5baf03c
--- /dev/null
+++ b/book/Tests/CtrGen/VectorTest/nil.kind2
@@ -0,0 +1,2 @@
+nil <T> : (Tests/CtrGen/VectorTest T Nat/zero) = 
+ ~λP λcons λnil (nil)
\ No newline at end of file
diff --git a/src/book/mod.rs b/src/book/mod.rs
index 334ead7..ca3bf22 100644
--- a/src/book/mod.rs
+++ b/src/book/mod.rs
@@ -72,11 +72,34 @@ impl Book {
         self.defs.insert(def_name.clone(), def_value.clone());
       }
       // Finds dependencies and loads them
-      for (_, def_term) in defs.defs.into_iter() {
+      for (def_name, def_term) in defs.defs.into_iter() {
         let mut dependencies = BTreeSet::new();
         def_term.get_free_vars(im::Vector::new(), &mut dependencies);
         for ref_name in dependencies {
           if let Err(_) = self.load(&base, &ref_name) {
+            // If `ref_name` is an unbound constructor of the ADT `def_term`,
+            // we can generate it.
+            let maybe_ctr = Term::constructor_code((&def_name, &def_term), &ref_name);
+
+            if let Some(ctr_code) = maybe_ctr {
+              let ctr_code = ctr_code.flatten(Some(80));
+
+              let file_name = format!("{}.kind2", ref_name.trim_end_matches('/'));
+              let file_path = std::path::Path::new(&file_name);
+              let err = || format!("ERROR: could not create file for generated constructor {ref_name}");
+
+              // Create folder structure
+              std::fs::create_dir_all(file_path.parent().ok_or_else(err)?).map_err(|_| err())?;
+              // Write constructor to its own file.
+              // It rewrites the file if it already exists.
+              // TODO: If the ADT definition does not type check, the wrong constructor
+              //       is still written to its own file. What should I do in this case?
+              std::fs::write(&file_name, ctr_code).map_err(|_| err())?;
+
+              self.load(&base, &ref_name)?;
+              continue;
+            }
+
             self.handle_unbound(&file, &ref_name)?;
           }
         }
@@ -120,3 +143,145 @@ impl Book {
   }
 
 }
+
+#[cfg(test)]
+mod tests {
+  use crate::*;
+
+  // TODO: this could be in the `sugar` module
+  fn extract_adt(t: &Term) -> &Term {
+    match t {
+      Term::Lam { bod, .. } => extract_adt(bod),
+      Term::Ann { val, .. } => extract_adt(val),
+      Term::Src { val, .. } => extract_adt(val),
+      // Found ADT
+      Term::Slf { .. } => t,
+      // Couldn't find ADT
+      _ => t,
+    }
+  }
+
+  // TODO: this could be in the `term` module
+  fn apply(t: &Term, f: impl Fn(&Term) -> Term) -> Term {
+    match t {
+      Term::All { era, nam, inp, bod } => {
+        Term::All { era: *era, nam: nam.clone(), inp: Box::new(f(inp)), bod: Box::new(f(bod)) }
+      }
+      Term::Lam { era, nam, bod } => Term::Lam { era: *era, nam: nam.clone(), bod: Box::new(f(bod)) },
+      Term::App { era, fun, arg } => Term::App { era: *era, fun: Box::new(f(fun)), arg: Box::new(f(arg)) },
+      Term::Ann { chk, val, typ } => Term::Ann { chk: *chk, val: Box::new(f(val)), typ: Box::new(f(typ)) },
+      Term::Slf { nam, typ, bod } => {
+        Term::Slf { nam: nam.clone(), typ: Box::new(f(typ)), bod: Box::new(f(bod)) }
+      }
+      Term::Ins { val } => Term::Ins { val: Box::new(f(val)) },
+      Term::Set => Term::Set,
+      Term::U60 => Term::U60,
+      Term::Num { val } => Term::Num { val: *val },
+      Term::Op2 { opr, fst, snd } => Term::Op2 { opr: *opr, fst: Box::new(f(fst)), snd: Box::new(f(snd)) },
+      Term::Swi { nam, x, z, s, p } => Term::Swi {
+        nam: nam.clone(),
+        x: Box::new(f(x)),
+        z: Box::new(f(z)),
+        s: Box::new(f(s)),
+        p: Box::new(f(p)),
+      },
+      Term::Nat { nat } => Term::Nat { nat: *nat },
+      Term::Txt { txt } => Term::Txt { txt: txt.clone() },
+      Term::Let { nam, val, bod } => {
+        Term::Let { nam: nam.clone(), val: Box::new(f(val)), bod: Box::new(f(bod)) }
+      }
+      Term::Use { nam, val, bod } => {
+        Term::Use { nam: nam.clone(), val: Box::new(f(val)), bod: Box::new(f(bod)) }
+      }
+      Term::Var { nam } => Term::Var { nam: nam.clone() },
+      Term::Hol { nam } => Term::Hol { nam: nam.clone() },
+      Term::Met {} => Term::Met {},
+      Term::Src { src, val } => Term::Src { src: src.clone(), val: Box::new(f(val)) },
+      Term::Mch { mch } => f(&Term::new_match(mch)),
+    }
+  }
+
+  // TODO: this could be used to implement term equality
+  fn rename_variables(t: &Term, i: usize, uses: &Uses) -> Term {
+    match t {
+      Term::Lam { era, nam, bod } => match uses.get(nam) {
+        Some(nam) => Term::Lam {
+          era: *era,
+          nam: nam.clone(),
+          bod: Box::new(rename_variables(bod, i, uses))
+        },
+        None => {
+          let new_nam = format!("x{i}");
+          Term::Lam {
+            era: *era,
+            nam: new_nam.clone(),
+            bod: Box::new(rename_variables(bod, i + 1, &uses.update(nam.clone(), new_nam))),
+          }
+        }
+      },
+      Term::Var { nam } => Term::Var { nam: uses.get(nam).unwrap_or(nam).clone() },
+      _ => apply(t, |t| rename_variables(t, i, uses)),
+    }
+  }
+
+  #[test]
+  /// Test if construction generation matches book
+  fn constructor_generation() {
+    let book_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("book");
+    let modules_to_test = [
+      "BBT",
+      "BMap",
+      "Bool",
+      "Char",
+      "Cmp",
+      "Empty",
+      "Equal",
+      "List",
+      "Maybe",
+      "Monad",
+      "Nat",
+      "Pair",
+      "String",
+      "Vector",
+      "Tests/CtrGen/ParamsTest",
+      "Tests/CtrGen/VectorTest",
+    ];
+
+    for module in modules_to_test {
+      println!("Testing module `{module}`.");
+      let mut book = Book::boot(&book_dir.to_string_lossy(), module).unwrap();
+      // Needed because some constructors are loaded as ADT.cons instead of ADT/cons
+      book.defs = book.defs.into_iter().map(|(key, val)| (key.replace(".", "/"), val)).collect();
+
+      for (_, term) in book.defs.iter() {
+        if let Some(adt) = extract_adt(term).as_adt() {
+          println!("Testing ADT `{}`.", adt.name);
+          let full_name = |adt_name: &str, ctr_name: &str| format!("{adt_name}/{ctr_name}");
+
+          let ctrs: Vec<(&str, &Term)> = adt
+            .ctrs
+            .iter()
+            .map(|ctr| {
+              let name = full_name(&adt.name, &ctr.name);
+              (ctr.name.as_ref(), book.defs.get(&name).expect(&format!("couldn't find {name}")))
+            })
+            .collect();
+
+          for (ctr_name, ctr_term) in ctrs {
+            println!("Testing constructor {ctr_name}");
+
+            let ctr_ref = full_name(&adt.name, ctr_name);
+            let gen_code = Term::constructor_code((&adt.name, term), &ctr_ref).unwrap();
+            let gen_term =
+              KindParser::new(&gen_code.flatten(None)).parse_def(0, &im::HashMap::new()).unwrap().1;
+
+            let t1 = rename_variables(ctr_term, 0, &im::HashMap::new());
+            let t2 = rename_variables(&gen_term, 0, &im::HashMap::new());
+            assert_eq!(t1.show(), t2.show());
+          }
+        }
+      }
+      println!();
+    }
+  }
+}
diff --git a/src/show/mod.rs b/src/show/mod.rs
index 19b062d..568fc9c 100644
--- a/src/show/mod.rs
+++ b/src/show/mod.rs
@@ -128,7 +128,7 @@ impl Show {
           },
           Style::Glue => {
             for (i, c) in child.iter().enumerate() {
-              if i > 0 {
+              if i > 0 && !c.is_empty() {
                 out.push_str(&join);
               }
               c.flatten_into(out, fmt, tab, lim);
@@ -162,6 +162,18 @@ impl Show {
     }
   }
 
+  // Checks if the element contains no text.
+  fn is_empty(&self) -> bool {
+    match self {
+      Show::Many { child, .. } => child.is_empty(),
+      Show::Text { value } => value.is_empty(),
+      Show::Line => false,
+      Show::Semi => false,
+      Show::Inc => false,
+      Show::Dec => false,
+    }
+  }
+
   // Sums the width of all children ropes, up to a limit.
   fn width(&self, lim: usize) -> usize {
     let mut total_width = 0;
diff --git a/src/sugar/mod.rs b/src/sugar/mod.rs
index 941de0b..7e6fb55 100644
--- a/src/sugar/mod.rs
+++ b/src/sugar/mod.rs
@@ -394,7 +394,6 @@ impl<'i> KindParser<'i> {
 // ---
 
 impl Term {
-
   // Interprets a λ-encoded Algebraic Data Type definition as an ADT struct.
   pub fn as_adt(&self) -> Option<ADT> {
     let name: String;
@@ -662,6 +661,89 @@ impl Term {
     return term;
   }
 
+  pub fn constructor_code((adt_name, adt_term): (&str, &Term), ctr_ref: &str) -> Option<Box<Show>> {
+    // Check if `adt_name` really is an ADT
+    let adt = match &adt_term {
+      // Type variables wrap ADTs in Lams
+      Term::Lam { bod, .. } => return Term::constructor_code((adt_name, bod), ctr_ref),
+      // Skip `Ann` and `Src`
+      Term::Ann { val, .. } => return Term::constructor_code((adt_name, val), ctr_ref),
+      Term::Src { val, .. } => return Term::constructor_code((adt_name, val), ctr_ref),
+      // Found an ADT
+      Term::Slf { .. } => adt_term.as_adt()?,
+      _ => return None,
+    };
+
+    let ctrs = adt.ctrs.clone();
+
+    // Search for constructor in ADT
+    let ctr_ref = ctr_ref.trim_end_matches('/'); // last "/" is not part of name
+    let ctr = ctrs.iter().find(|ctr| format!("{adt_name}/{}", ctr.name) == ctr_ref)?.clone();
+
+    // Generate constructor code:
+
+    // Constructor name.
+    let ctr_name = &ctr.name;
+
+    // Type parameters.
+    // Format: <Par_1> .. <Par_n>
+    let format_param = |param| Show::text(&format!("<{}>", param));
+    let params = Show::glue(" ", adt.pars.iter().map(format_param).rev().collect());
+
+    // Constructor fields.
+    // Format: (f_1: T_1) .. (f_n: T_n)
+    let format_field = |(name, typ): &(String, Term)| {
+      Show::glue("", vec![
+        Show::text("("),
+        Show::glue("", vec![Show::text(name), Show::text(": "), typ.format()]),
+        Show::text(")"),
+      ])
+    };
+    let fields = Show::glue(" ", ctr.flds.iter().map(format_field).collect());
+
+    // Constructor return type with type parameters and type indices.
+    // Format: (adt_name Par_1 .. Par_n Idx_1 .. Idx_n)
+    let mut ctr_typ = vec![Show::text(&adt.name)];
+    adt.pars.iter().rev().for_each(|par| ctr_typ.push(Show::text(par)));
+    ctr.idxs.iter().rev().for_each(|idx| ctr_typ.push(idx.format()));
+    let ctr_typ = Show::glue("", vec![Show::text("("), Show::glue(" ", ctr_typ), Show::text(")")]);
+
+    // Constructor names into Scott-encoding.
+    // Format: λctr_name_1 .. λctr_name_n
+    let format_ctr_lam_name = |ctr_name| Show::text(&format!("λ{ctr_name}"));
+    let names = ctrs.into_iter().map(|ctr| ctr.name);
+    let ctr_lam_names = Show::glue(" ", names.map(format_ctr_lam_name).collect());
+
+    // Fields without their types.
+    // Format: f_1 .. f_n
+    let field_names = Show::glue(" ", ctr.flds.iter().map(|(name, _)| Show::text(name)).collect());
+
+    // Applies constructor and fields.
+    // Format: (ctr_name f_1 .. f_n)
+    let final_app = Show::glue("", vec![
+      Show::text("("),
+      Show::glue(" ", vec![Show::text(ctr_name), field_names]),
+      Show::text(")"),
+    ]);
+
+    // The result should be in the following format:
+    // ctr_name <Par_1> .. <Par_n> (f_1: T_1) .. (f_n: T_n): (adt_name Par_1 .. Par_n Idx_1 .. Idx_n) =
+    //   ~λP λctr_name_1 .. λctr_name_n (ctr_name f_1 .. f_n)
+    let ctr_text = Show::glue(" ", vec![
+      Show::text(ctr_name),
+      params,
+      fields,
+      Show::text(":"),
+      ctr_typ,
+      Show::text("="),
+      Show::line(),
+      Show::text("~λP"),
+      ctr_lam_names,
+      final_app,
+    ]);
+
+    Some(ctr_text)
+  }
 }
 
 impl ADT {