1 files changed, 7 insertions, 4 deletions
diff --git a/src/driver/Driver.ml b/src/driver/Driver.ml
index a2c4364..57eec82 100644
--- a/src/driver/Driver.ml
+++ b/src/driver/Driver.ml
@@ -1,9 +1,12 @@
 let process_item (toplvl : TopLevel.t) (item : Ast.item) : TopLevel.t =
   let (name, item) = match item with
-    | Ast.Def { name; tp; tm } ->
-      let tp = Elaborator.check_tp_toplevel ~toplvl tp in
-      let tm = Elaborator.check_toplevel ~toplvl ~tm ~tp in
-      (name, TopLevel.Def { tp; tm = lazy (NbE.eval_toplevel tm) })
+    | Ast.Def { name; args; tp; tm } ->
+      let (tp, tm) = Elaborator.check_def_toplevel ~toplvl ~args ~tp ~tm in
+      let item = TopLevel.Def {
+          tp = NbE.eval_toplevel tp;
+          tm = lazy (NbE.eval_toplevel tm);
+        } in
+      (name, item)
   in
   Yuujinchou.Trie.update_singleton name.value (fun _ -> Some (item, ())) toplvl