From 3cf472b13c9b329b711a5c254fc6f89268a99eda Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Mon, 8 Jul 2024 23:59:31 +0200
Subject: implement argument lists for top-level definitions

---
 src/driver/Driver.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'src/driver')

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
 
-- 
cgit 1.4.1