From a3094b55bb906cae6461f24ebafa91c355f1eb13 Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Tue, 22 Sep 2015 15:32:45 -0400
Subject: [PATCH] Fixed top

---
 curnel/redex-lang.rkt | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/curnel/redex-lang.rkt b/curnel/redex-lang.rkt
index 316dab1..55584d4 100644
--- a/curnel/redex-lang.rkt
+++ b/curnel/redex-lang.rkt
@@ -406,6 +406,7 @@
 (define-syntax (dep-inductive syn)
   (syntax-case syn (:)
     [(_ i : ti (x1 : t1) ...)
+     ;; TODO: Probably should occur only in definition context? and also, should not really produce void
      (begin
        (extend-Σ/syn! sigma #'i #'ti #'((x1 : t1) ...))
        #'(void))]))
@@ -419,7 +420,7 @@
 ;; TODO: Not sure if this is the correct behavior for #%top
 (define-syntax (dep-top syn)
   (syntax-case syn ()
-    [(_ . id) (denote syn #'id)]))
+    [(_ . id) (normalize/syn #'id)]))
 
 ;; TODO: Syntax-parse
 (define-syntax (dep-define syn)