Fixed top

This commit is contained in:
William J. Bowman 2015-09-22 15:32:45 -04:00
parent 722ac7d68f
commit a3094b55bb
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A

View File

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