add ?∀ and ?Λ

This commit is contained in:
AlexKnauth 2016-05-03 11:00:41 -04:00
parent 95d960267a
commit e243ee0656

View File

@ -31,6 +31,25 @@
;; - pattern matching
;; - (local) type inference
;; creating possibly polymorphic types
;; ?∀ only wraps a type in a forall if there's at least one type variable
(define-syntax ?∀
(lambda (stx)
(syntax-case stx ()
[(?∀ () body)
#'body]
[(?∀ (X ...) body)
#'( (X ...) body)])))
;; ?Λ only wraps an expression in a Λ if there's at least one type variable
(define-syntax
(lambda (stx)
(syntax-case stx ()
[( () body)
#'body]
[( (X ...) body)
#'(Λ (X ...) body)])))
(begin-for-syntax
;; matching possibly polymorphic types
(define-syntax ~?∀