diff --git a/parser/src/command.rs b/parser/src/command.rs
index 64017f083256704196734cecee459f0a192008e4..3f3c1fc162d5b2bf81e3538b1bbe431d0c5b3250 100644
--- a/parser/src/command.rs
+++ b/parser/src/command.rs
@@ -10,6 +10,9 @@ use kernel::memory::term::builder::Builder;
 /// The type of commands that can be received by the kernel.
 #[derive(Debug, Eq, PartialEq)]
 pub enum Command<'build> {
+    /// Define the given term
+    Define(&'build str, Option<Builder<'build>>, Builder<'build>),
+
     /// Define the given declaration
     Declaration(&'build str, Option<declaration::Builder<'build>>, declaration::Builder<'build>),
 
@@ -34,6 +37,10 @@ impl<'build> fmt::Display for Command<'build> {
         use Command::*;
 
         match self {
+            Define(name, None, t) => write!(f, "def {name} := {t}"),
+
+            Define(name, Some(ty), t) => write!(f, "def {name}: {ty} := {t}"),
+
             Declaration(name, None, t) => write!(f, "def {name} := {t}"),
 
             Declaration(name, Some(ty), t) => write!(f, "def {name}: {ty} := {t}"),
diff --git a/parser/src/parser.rs b/parser/src/parser.rs
index db73e6c7242bf07b3646e997739315a364a5abae..a997617fb08d9b2ad977c9a3854edbc725e64730 100644
--- a/parser/src/parser.rs
+++ b/parser/src/parser.rs
@@ -161,19 +161,16 @@ fn parse_expr(pair: Pair<Rule>) -> Command {
             let mut iter = pair.into_inner();
             let s = iter.next().unwrap().as_str();
             let term = parse_term(iter.next().unwrap());
-            Command::Declaration(s, None, declaration::Builder::Decl(box term, Vec::new()))
+            Command::Define(s, None, term)
         },
 
         Rule::DefineCheckType => {
             let mut iter = pair.into_inner();
             let s = iter.next().unwrap().as_str();
             let ty = parse_term(iter.next().unwrap());
-            let decl = parse_term(iter.next().unwrap());
-
-            let ty = declaration::Builder::Decl(box ty, Vec::new());
-            let decl = declaration::Builder::Decl(box decl, Vec::new());
+            let term = parse_term(iter.next().unwrap());
 
-            Command::Declaration(s, Some(ty), decl)
+            Command::Define(s, Some(ty), term)
         },
 
         Rule::Declaration => {
@@ -336,14 +333,7 @@ mod tests {
 
     #[test]
     fn successful_define_with_type_annotation() {
-        assert_eq!(
-            parse_line("def x : Type := Prop"),
-            Ok(Declaration(
-                "x",
-                Some(declaration::Builder::Decl(box Type(box level::Builder::Const(0)), Vec::new())),
-                declaration::Builder::Decl(box Prop, Vec::new())
-            ))
-        );
+        assert_eq!(parse_line("def x : Type := Prop"), Ok(Define("x", Some(Type(box level::Builder::Const(0))), Prop)));
     }
 
     #[test]
@@ -382,7 +372,7 @@ mod tests {
 
     #[test]
     fn successful_define() {
-        assert_eq!(parse_line("def x := Prop"), Ok(Declaration("x", None, declaration::Builder::Decl(box Prop, Vec::new()))));
+        assert_eq!(parse_line("def x := Prop"), Ok(Define("x", None, Prop)));
     }
 
     #[test]
diff --git a/proost/src/evaluator.rs b/proost/src/evaluator.rs
index 38947a6789c2cc96082048f42e7f030649054343..89a00c19e6eda64fce2e143e261c0cfa9abefad8 100644
--- a/proost/src/evaluator.rs
+++ b/proost/src/evaluator.rs
@@ -132,40 +132,47 @@ impl<'arena> Evaluator {
             .map(|_| None)
     }
 
-    fn process<'build>(
+    fn process(
         &mut self,
         arena: &mut Arena<'arena>,
-        command: &Command<'build>,
+        command: &Command,
         importing: &mut Vec<PathBuf>,
     ) -> Result<'arena, Option<Term<'arena>>> {
         match command {
-            Command::Declaration(s, None, decl) => {
-                let decl = decl.realise(arena)?;
-                if arena.get_binding(s).is_none() {
-                    decl.infer(arena)?;
-                    arena.bind_decl(s, decl);
-                    Ok(None)
-                } else {
-                    Err(Toplevel(Error {
+            Command::Define(s, ty, term) => {
+                if arena.get_binding(s).is_some() {
+                    return Err(Toplevel(Error {
                         kind: ErrorKind::BoundVariable(s.to_string()),
                         location: Location::default(), // TODO (see #38)
-                    }))
+                    }));
+                }
+                let term = term.realise(arena)?;
+                match ty {
+                    None => {
+                        term.infer(arena)?;
+                    },
+                    Some(ty) => term.check(ty.realise(arena)?, arena)?,
                 }
+                arena.bind(s, term);
+                Ok(None)
             },
 
-            Command::Declaration(s, Some(t), decl) => {
-                let decl = decl.realise(arena)?;
-                let ty = t.realise(arena)?;
-                if arena.get_binding(s).is_none() {
-                    decl.check(ty, arena)?;
-                    arena.bind_decl(s, decl);
-                    Ok(None)
-                } else {
-                    Err(Toplevel(Error {
+            Command::Declaration(s, ty, decl) => {
+                if arena.get_binding_decl(s).is_some() {
+                    return Err(Toplevel(Error {
                         kind: ErrorKind::BoundVariable(s.to_string()),
                         location: Location::default(), // TODO (see #38)
-                    }))
+                    }));
                 }
+                let decl = decl.realise(arena)?;
+                match ty {
+                    None => {
+                        decl.infer(arena)?;
+                    },
+                    Some(ty) => decl.check(ty.realise(arena)?, arena)?,
+                }
+                arena.bind_decl(s, decl);
+                Ok(None)
             },
 
             Command::CheckType(t1, t2) => {