fix the type of run-ground-dataspace
This commit is contained in:
parent
bdf4c30218
commit
e5b797b450
|
@ -577,8 +577,9 @@
|
||||||
[⊢ s ≫ s- (⇒ : t1)] ...
|
[⊢ s ≫ s- (⇒ : t1)] ...
|
||||||
[⊢ (dataspace τ-c.norm s- ...) ≫ _ (⇒ : t2)]
|
[⊢ (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
|
;; Utilities
|
||||||
|
|
Loading…
Reference in New Issue