diff --git a/racket/typed/for-loops.rkt b/racket/typed/for-loops.rkt index b3d5d29..3d2b537 100644 --- a/racket/typed/for-loops.rkt +++ b/racket/typed/for-loops.rkt @@ -5,7 +5,9 @@ for/list for/set for/sum - for/first) + for/first + in-hash-values + in-hash-keys) (require "core-types.rkt") (require "sequence.rkt") @@ -223,3 +225,14 @@ (⇒ ν-ep (τ-ep ...)) (⇒ ν-s (τ-s ...)) (⇒ ν-f (τ-f ...))]) + + +(define-typed-syntax (in-hash-values h) ≫ + [⊢ h ≫ h- (⇒ : (~Hash K V))] + -------------------- + [⊢ (#%app- in-hash-values- h-) (⇒ : (Sequence V))]) + +(define-typed-syntax (in-hash-keys h) ≫ + [⊢ h ≫ h- (⇒ : (~Hash K V))] + -------------------- + [⊢ (#%app- in-hash-keys- h-) (⇒ : (Sequence K))])