From e5b797b450eb60a6d1a2358dc10f9bf4a0d226cd Mon Sep 17 00:00:00 2001 From: Sam Caldwell Date: Thu, 22 Oct 2020 16:46:48 -0400 Subject: [PATCH] fix the type of run-ground-dataspace --- racket/typed/roles.rkt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt index 9889192..b2e9750 100644 --- a/racket/typed/roles.rkt +++ b/racket/typed/roles.rkt @@ -577,8 +577,9 @@ [⊢ s ≫ s- (⇒ : t1)] ... [⊢ (dataspace τ-c.norm s- ...) ≫ _ (⇒ : t2)] ] + #:with τ-out (strip-outbound #'τ-c.norm) ----------------------------------------------------------------------------------- - [⊢ (#%app- syndicate:run-ground s- ...) (⇒ : (AssertionSet τ-c))]) + [⊢ (#%app- syndicate:run-ground s- ...) (⇒ : (AssertionSet τ-out))]) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Utilities