diff --git a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
index 6ad4ccdc33..93ba3a2c5b 100644
--- a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
+++ b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
@@ -2952,18 +2952,22 @@ other tools that combine @racketmodname[pict]s together.
 }
 
 @deftogether[[
-@defform[(render-metafunction metafunction-name)]{}
+@defform[(render-metafunction metafunction-name maybe-contract)]{}
 @defform/none[#:literals (render-metafunction)
-              (render-metafunction metafunction-name filename)]{}
-@defform[(render-metafunctions metafunction-name ...)]{}
-@defform/none[#:literals (render-metafunctions)
-              (render-metafunctions metafunction-name ... #:file filename)]{}]]{
+              (render-metafunction metafunction-name filename maybe-contract)]{}
+@defform[(render-metafunctions metafunction-name ... maybe-filename maybe-contract)
+          #:grammar ([maybe-filename (code:line) (code:line #:file filename)]
+                     [maybe-contract? (code:line) (code:line #:contract? bool-expr)])]{}]]{
 Like @racket[render-reduction-relation] but for metafunctions.
 
 Similarly, @racket[render-metafunctions] accepts multiple 
 metafunctions and renders them together, lining up all of the
 clauses together.
 
+If the metafunctions have contracts, they are typeset as the first
+lines of the output, unless the expression following @racket[#:contract?]
+evaluates to @racket[#f].
+
 This function sets @racket[dc-for-text-size]. See also
 @racket[metafunction->pict] and
 @racket[metafunctions->pict].
@@ -3146,10 +3150,10 @@ precede ellipses that represent argument sequences; when it is
   are rendered on two lines and which are rendered on one.
   
   If its value is a list, the length of the list must match
-  the number of cases and each boolean indicates if that
-  case has a linebreak or not.
+  the number of cases plus one if there is a contract. 
+  Each boolean indicates if that case has a linebreak or not.
   
-  This influences the @racket['left/right] styles only.
+  This parameter's value influences the @racket['left/right] styles only.
 }
 
 @defparam[metafunction-cases 
diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt
index 48320333a6..bf88b8af0b 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt
@@ -407,7 +407,7 @@
      (begin
        (unless (identifier? #'lang)
          (raise-syntax-error #f "expected an identifier in the language position" stx #'lang))
-       (define-values (contract-name dom-ctcs codom-contracts pats)
+       (define-values (contract-name dom-ctcs pre-condition codom-contracts pats)
          (split-out-contract stx (syntax-e #'def-form-id) #'body #t))
        (with-syntax* ([((name trms ...) rest ...) (car pats)]
                       [(mode-stx ...) #`(#:mode (name I))]
@@ -416,7 +416,7 @@
                                          #'())]
                       [(clauses ...) pats]
                       [new-body #`(mode-stx ... ctc-stx ... clauses ...)])
-                     (do-extended-judgment-form #'lang (syntax-e #'def-form-id) #'new-body #f stx #t)))]))
+         (do-extended-judgment-form #'lang (syntax-e #'def-form-id) #'new-body #f stx #t)))]))
 
 ;; if relation? is true, then the contract is a list of redex patterns
 ;; if relation? is false, then the contract is a single redex pattern
@@ -425,7 +425,7 @@
   ;; initial test determines if a contract is specified or not
   (cond
     [(pair? (syntax-e (car (syntax->list rest))))
-     (values #f #f (list #'any) (check-clauses stx syn-error-name (syntax->list rest) relation?))]
+     (values #f #f #f (list #'any) (check-clauses stx syn-error-name (syntax->list rest) relation?))]
     [else
      (syntax-case rest ()
        [(id separator more ...)
@@ -438,7 +438,7 @@
                (raise-syntax-error syn-error-name 
                                    "expected clause definitions to follow domain contract"
                                    stx))
-             (values #'id contract (list #'any) (check-clauses stx syn-error-name clauses #t)))]
+             (values #'id contract #f (list #'any) (check-clauses stx syn-error-name clauses #t)))]
           [else
            (unless (eq? ': (syntax-e #'separator))
              (raise-syntax-error syn-error-name "expected a colon to follow the meta-function's name" stx #'separator))
@@ -481,10 +481,9 @@
                                      #t)])])])))
                 (let ([doms (reverse dom-pats)]
                       [clauses (check-clauses stx syn-error-name raw-clauses relation?)])
-                  (values #'id 
-                          (if relation?
-                              doms
-                              #`(side-condition #,doms (term #,pre-condition)))
+                  (values #'id
+                          doms
+                          (if relation? #f pre-condition)
                           (reverse rev-codomains)
                           clauses))]
                [else
diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt
index 4bcd7c2317..67b754d656 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt
@@ -1187,7 +1187,7 @@
           prev-metafunction
           (λ ()
             (raise-syntax-error syn-error-name "expected a previously defined metafunction" orig-stx prev-metafunction))))
-       (let*-values ([(contract-name dom-ctcs codom-contracts pats)
+       (let*-values ([(contract-name dom-ctcs pre-condition codom-contracts pats)
                       (split-out-contract orig-stx syn-error-name #'rest #f)]
                      [(name _) (defined-name (list contract-name) pats orig-stx)])
          (when (and prev-metafunction (eq? (syntax-e #'name) (syntax-e prev-metafunction)))
@@ -1208,6 +1208,7 @@
                                                               name
                                                               name-predicate
                                                               #,dom-ctcs
+                                                              #,pre-condition
                                                               #,codom-contracts
                                                               #,pats
                                                               #,syn-error-name))
@@ -1251,9 +1252,13 @@
 
 (define-syntax (generate-metafunction stx)
   (syntax-case stx ()
-    [(_ orig-stx lang prev-metafunction name name-predicate dom-ctcs codom-contracts pats syn-error-name)
+    [(_ orig-stx lang prev-metafunction 
+        name name-predicate
+        dom-ctcs pre-condition
+        codom-contracts pats syn-error-name)
      (let ([prev-metafunction (and (syntax-e #'prev-metafunction) #'prev-metafunction)]
            [dom-ctcs (syntax-e #'dom-ctcs)]
+           [pre-condition (syntax-e #'pre-condition)]
            [codom-contracts (syntax-e #'codom-contracts)]
            [pats (syntax-e #'pats)]
            [syn-error-name (syntax-e #'syn-error-name)])
@@ -1323,7 +1328,7 @@
                                      #'lang
                                      syn-error-name
                                      #f
-                                     dom-ctcs)
+                                     #`(side-condition #,dom-ctcs (term #,pre-condition)))
                                     #'((void) any () ()))]
                                [((codom-syncheck-expr codom-side-conditions-rewritten codom-names codom-names/ellipses) ...)
                                 (map (λ (codom-contract)
@@ -1369,7 +1374,6 @@
                                 #,(if prev-metafunction
                                       #`(metafunc-proc-cases #,(term-fn-get-id (syntax-local-value prev-metafunction)))
                                       #'null)])
-                           
                            (build-metafunction 
                             lang
                             cases
@@ -1378,12 +1382,23 @@
                               (make-metafunc-proc
                                (let ([name (lambda (x) (f/dom x))]) name)
                                '(clause-name ...)
-                               (generate-lws #f
-                                             (lhs ...)
-                                             (lhs-for-lw ...)
-                                             ((stuff ...) ...)
-                                             (rhs ...)
-                                             #t)
+                               (list
+                                ;; mf contract
+                                #,(if (and dom-ctcs codom-contracts)
+                                      #`(list
+                                         #,(with-syntax ([(dom-ctc ...) dom-ctcs])
+                                             #`(list (to-lw dom-ctc) ...))
+                                         #,(with-syntax ([(codom-ctc ...) codom-contracts])
+                                             #`(list (to-lw codom-ctc) ...)))
+                                      #'#f)
+                                
+                                ;; body of mf
+                                (generate-lws #f
+                                              (lhs ...)
+                                              (lhs-for-lw ...)
+                                              ((stuff ...) ...)
+                                              (rhs ...)
+                                              #t))
                                lang
                                #t ;; multi-args?
                                'name
diff --git a/pkgs/redex-pkgs/redex-pict-lib/redex/private/pict.rkt b/pkgs/redex-pkgs/redex-pict-lib/redex/private/pict.rkt
index f9bb2a7656..f078e3bc95 100644
--- a/pkgs/redex-pkgs/redex-pict-lib/redex/private/pict.rkt
+++ b/pkgs/redex-pkgs/redex-pict-lib/redex/private/pict.rkt
@@ -5,7 +5,7 @@
          racket/match
          racket/pretty
          racket/set
-         (only-in racket/list drop-right last partition)
+         (only-in racket/list drop-right last partition add-between)
          
          texpict/mrpict
          texpict/utils
@@ -21,7 +21,8 @@
          (prefix-in lw/rt: redex/private/loc-wrapper-rt))
 
 (require (for-syntax racket/base
-                     redex/private/term-fn))
+                     redex/private/term-fn
+                     syntax/parse))
 
 (provide render-term 
          term->pict
@@ -261,7 +262,6 @@
         (apply
          vl-append
          (add-between
-          (blank 0 (reduction-relation-rule-separation))
           (map (λ (rp)
                  (side-condition-combiner
                   (vl-append
@@ -274,7 +274,8 @@
                      (rp->pict-label rp)))
                    (rule-pict-rhs rp))
                   (rp->side-condition-pict rp +inf.0)))
-               rps))))))
+               rps)
+          (blank 0 (reduction-relation-rule-separation)))))))
 
 (define compact-vertical-min-width (make-parameter 0))
 
@@ -352,14 +353,14 @@
                 (apply 
                  hbl-append
                  (add-between
-                  (basic-text ", " (default-style))
-                  fresh-vars))
+                  fresh-vars
+                  (basic-text ", " (default-style))))
                 (basic-text " fresh" (default-style)))))]
          [lst (add-between
-               'comma
                (append
                 pattern-binds/sc
-                frsh))])
+                frsh)
+               'comma)])
     (if (null? lst)
         (blank)
         (let ([where ((where-make-prefix-pict))])
@@ -414,14 +415,6 @@
    label
    ((current-text) "]" (label-style) (label-font-size))))
 
-(define (add-between i l)
-  (cond
-    [(null? l) l]
-    [else 
-     (cons (car l)
-           (apply append 
-                  (map (λ (x) (list i x)) (cdr l))))]))
-
 (define (make-horiz-space picts) (blank (pict-width (apply cc-superimpose picts)) 0))
 
 (define rule-pict-style (make-parameter 'vertical))
@@ -773,11 +766,11 @@
      #'(metafunctions->pict name)]))
 
 (define-syntax (metafunctions->pict stx)
-  (syntax-case stx ()
-    [(_ name1 name2 ...)
-     (and (identifier? #'name1)
-          (andmap identifier? (syntax->list #'(name2 ...))))
-     #'(metafunctions->pict/proc (list (metafunction name1) (metafunction name2) ...) 'metafunctions->pict)]))
+  (syntax-parse stx 
+    [(_ name1:id name2:id ... (~optional (~seq #:contract? contract-e:expr) #:defaults ([contract-e #'#t])))
+     #'(metafunctions->pict/proc (list (metafunction name1) (metafunction name2) ...)
+                                 contract-e
+                                 'metafunctions->pict)]))
 
 (define-syntax (relation->pict stx)
   (syntax-case stx ()
@@ -786,24 +779,39 @@
      #'(inference-rules-pict/relation 'form (metafunction name1))]))
 
 (define-syntax (render-metafunctions stx)
-  (syntax-case stx ()
-    [(_ name1 name2 ...)
-     (and (identifier? #'name)
-          (andmap identifier? (syntax->list #'(name2 ...))))
-     #'(render-metafunction/proc (list (metafunction name1) (metafunction name2) ...) #f 'render-metafunctions)]
-    [(_ name1 name2 ... #:file filename)
-     (and (identifier? #'name1)
-          (andmap identifier? (syntax->list #'(name2 ...))))
-     #'(render-metafunction/proc (list (metafunction name1) (metafunction name2) ...) filename 'render-metafunctions)]))
+  (syntax-parse stx
+    [(_ name1:id name2:id ... (~seq k:keyword e:expr) ...)
+     (define filename #'#f)
+     (define contract? #'#t)
+     (for ([kwd (in-list (syntax->list #'(k ...)))]
+           [e (in-list (syntax->list #'(e ...)))])
+       (cond
+         [(equal? '#:filename (syntax-e kwd))
+          (set! filename e)]
+         [(equal? '#:contract? (syntax-e kwd))
+          (set! contract? e)]
+         [else
+          (raise-syntax-error #f "unexpected keyword" stx kwd)]))
+     #`(render-metafunction/proc 
+        (list (metafunction name1) (metafunction name2) ...)
+        #,contract?
+        #,filename
+        'render-metafunctions)]))
 
 (define-syntax (render-metafunction stx)
-  (syntax-case stx ()
-    [(_ name)
-     (identifier? #'name)
-     #'(render-metafunction/proc (list (metafunction name)) #f 'render-metafunction)]
-    [(_ name file)
-     (identifier? #'name)
-     #'(render-metafunction/proc (list (metafunction name)) file 'render-metafunction)]))
+  (syntax-parse stx
+    [(_ name:id
+        (~optional file:expr #:defaults ([file #'#f]))
+        (~optional (~seq k:keyword e:expr)))
+     #`(render-metafunction/proc (list (metafunction name))
+                                 #,(cond
+                                     [(not (attribute k)) #'#f]
+                                     [(and (equal? (syntax-e (attribute k)) '#:contract?))
+                                      #'e]
+                                     [else
+                                      (raise-syntax-error #f "unknown keyword" stx #'k)])
+                                 file
+                                 'render-metafunction)]))
 
 (define-syntax (render-relation stx)
   (syntax-case stx ()
@@ -814,7 +822,7 @@
 
 (define metafunction-pict-style (make-parameter 'left-right))
 (define metafunction-cases (make-parameter #f))
-(define (select-mf-cases eqns case-labelss)
+(define (select-mf-cases contracts eqns case-labelss)
   (define mf-cases (metafunction-cases))
   (cond
     [mf-cases
@@ -824,21 +832,29 @@
      (apply 
       append
       (for/list ([eqns (in-list eqns)]
+                 [contract (in-list contracts)]
                  [case-labels (in-list case-labelss)])
         (filter
          values
-         (for/list ([eqn (in-list eqns)]
-                    [case-label (in-list case-labels)])
-           (begin0
-             (cond
-               [(and (pair? sorted-cases) (= i (car sorted-cases)))
-                (set! sorted-cases (cdr sorted-cases))
-                eqn]
-               [(set-member? named-cases case-label)
-                eqn]
-               [else #f])
-             (set! i (+ i 1)))))))]
-    [else (apply append eqns)]))
+         (cons 
+          contract
+          (for/list ([eqn (in-list eqns)]
+                     [case-label (in-list case-labels)])
+            (begin0
+              (cond
+                [(and (pair? sorted-cases) (= i (car sorted-cases)))
+                 (set! sorted-cases (cdr sorted-cases))
+                 eqn]
+                [(set-member? named-cases case-label)
+                 eqn]
+                [else #f])
+              (set! i (+ i 1))))))))]
+    [else (apply append 
+                 (for/list ([eqns (in-list eqns)]
+                            [contract (in-list contracts)])
+                   (if contract
+                       (cons contract eqns)
+                       eqns)))]))
 
 (define judgment-form-cases (make-parameter #f))
 (define (select-jf-cases eqns conclusions eqn-names)
@@ -877,9 +893,9 @@
       [else
        (cons (car l) (loop (cdr l)))])))
 
-(define (metafunctions->pict/proc mfs name)
-  (unless (andmap (λ (mf) (eq? (metafunc-proc-lang (metafunction-proc (car mfs)))
-                               (metafunc-proc-lang (metafunction-proc mf))))
+(define (metafunctions->pict/proc mfs contract? name)
+  (unless (andmap (λ (mf) (equal? (metafunc-proc-lang (metafunction-proc (car mfs)))
+                                  (metafunc-proc-lang (metafunction-proc mf))))
                   mfs)
     (error name "expected metafunctions that are all drawn from the same language"))
   (define current-linebreaks (linebreaks))
@@ -887,22 +903,39 @@
   (define sep 2)
   (define style (metafunction-pict-style))
   (define (wrapper->pict lw) (lw->pict all-nts lw))
-  (define all-eqns (map (λ (mf) (metafunc-proc-pict-info (metafunction-proc mf))) mfs))
+  (define contracts (for/list ([mf (in-list mfs)]) 
+                      (define lws (list-ref (metafunc-proc-pict-info (metafunction-proc mf)) 0))
+                      (cond
+                        [(and contract? lws)
+                         (define doms (list-ref lws 0))
+                         (define rngs (list-ref lws 1))
+                         (render-metafunction-contract
+                          (metafunc-proc-lang (metafunction-proc mf))
+                          (metafunc-proc-name (metafunction-proc mf))
+                          doms
+                          rngs)]
+                        [else #f])))
+  (define all-eqns (map (λ (mf) (list-ref (metafunc-proc-pict-info (metafunction-proc mf)) 1)) mfs))
   (define all-lhss 
-    (map (λ (mf)
-           (map (lambda (eqn) 
-                  (wrapper->pict
-                   (metafunction-call (metafunc-proc-name (metafunction-proc mf))
-                                      (list-ref eqn 0))))
-                (metafunc-proc-pict-info (metafunction-proc mf))))
-         mfs))
+    (for/list ([mf (in-list mfs)])
+      (for/list ([eqn (in-list (list-ref (metafunc-proc-pict-info (metafunction-proc mf)) 1))])
+        (wrapper->pict
+         (metafunction-call (metafunc-proc-name (metafunction-proc mf))
+                            (list-ref eqn 0))))))
   (define case-labels (map (λ (mf) (metafunc-proc-clause-names (metafunction-proc mf))) mfs))
-  (define eqns (select-mf-cases all-eqns case-labels))
-  (define lhss (select-mf-cases all-lhss case-labels))
-  (define rhss (map (lambda (eqn) (wrapper->pict (list-ref eqn 2))) eqns))
+  (define eqns (select-mf-cases contracts all-eqns case-labels))
+  (define lhs/contracts (select-mf-cases contracts all-lhss case-labels))
+  (define rhss (for/list ([eqn/contract (in-list eqns)])
+                 (if (pict? eqn/contract)
+                     'contract
+                     (wrapper->pict (list-ref eqn/contract 2)))))
   (unless (or (not current-linebreaks)
               (= (length current-linebreaks) (length eqns)))
-    (error 'metafunction->pict "expected the current-linebreaks parameter to be a list whose length matches the number of cases in the metafunction (~a), but got ~s"
+    (error 'metafunction->pict
+           (string-append
+            "expected the current-linebreaks parameter to be a list"
+            " whose length matches the number of cases in the metafunction"
+            " plus one if there is a contract (~a), but got ~s")
            (length eqns)
            current-linebreaks))
   (define linebreak-list (or current-linebreaks
@@ -923,45 +956,55 @@
                   left-right*/compact-side-conditions)))
   (define max-line-w/pre-sc (and
                              compact-side-conditions?
-                             (apply
-                              max
-                              (map (lambda (lhs rhs linebreak?)
-                                     (cond
-                                      [(eq? mode 'vertical)
-                                       (max (+ (pict-width lhs) (pict-width =-pict))
-                                            (pict-width rhs))]
-                                      [linebreak?
-                                       (max (pict-width lhs)
-                                            (+ (pict-width rhs) sep (pict-width =-pict)))]
-                                      [else
-                                       (+ (pict-width lhs) (pict-width rhs) (pict-width =-pict)
-                                          (* 2 sep))]))
-                                   lhss rhss linebreak-list))))
+                             (for/fold ([biggest 0]) ([lhs/contract (in-list lhs/contracts)]
+                                                      [rhs (in-list rhss)]
+                                                      [linebreak? (in-list linebreak-list)])
+                               (cond
+                                 [(equal? rhs 'contract)
+                                  ;; this is a contract
+                                  (max biggest (pict-width lhs/contract))]
+                                 [(eq? mode 'vertical)
+                                  (max biggest
+                                       (+ (pict-width lhs/contract) (pict-width =-pict))
+                                       (pict-width rhs))]
+                                 [linebreak?
+                                  (max biggest
+                                       (pict-width lhs/contract)
+                                       (+ (pict-width rhs) sep (pict-width =-pict)))]
+                                 [else
+                                  (max biggest
+                                       (+ (pict-width lhs/contract) (pict-width rhs) (pict-width =-pict)
+                                          (* 2 sep)))]))))
   (define scs (for/list ([eqn (in-list eqns)])
-                (let ([scs (reverse (list-ref eqn 1))])
-                  (if (null? scs)
-                      #f
-                      (let-values ([(fresh where/sc) (partition metafunc-extra-fresh? scs)])
-                        (side-condition-pict (foldl (λ (clause picts) 
-                                                      (foldr (λ (l ps) (cons (wrapper->pict l) ps))
-                                                             picts (metafunc-extra-fresh-vars clause)))
-                                                    '() fresh)
-                                             (map (match-lambda
-                                                    [(struct metafunc-extra-where (lhs rhs))
-                                                     (where-pict (wrapper->pict lhs) (wrapper->pict rhs))]
-                                                    [(struct metafunc-extra-side-cond (expr))
-                                                     (wrapper->pict expr)])
-                                                  where/sc)
-                                             (cond
-                                               [vertical-side-conditions? 
-                                                ;; maximize line breaks:
-                                                0]
-                                               [compact-side-conditions?
-                                                ;; maximize line break as needed:
-                                                max-line-w/pre-sc]
-                                               [else 
-                                                ;; no line breaks:
-                                                +inf.0])))))))
+                (cond
+                  [(pict? eqn) #f]
+                  [else
+                   (define scs (reverse (list-ref eqn 1)))
+                   (cond
+                     [(null? scs) #f]
+                     [else
+                      (define-values (fresh where/sc) (partition metafunc-extra-fresh? scs))
+                      (side-condition-pict 
+                       (foldl (λ (clause picts) 
+                                (foldr (λ (l ps) (cons (wrapper->pict l) ps))
+                                       picts (metafunc-extra-fresh-vars clause)))
+                              '() fresh)
+                       (map (match-lambda
+                              [(struct metafunc-extra-where (lhs rhs))
+                               (where-pict (wrapper->pict lhs) (wrapper->pict rhs))]
+                              [(struct metafunc-extra-side-cond (expr))
+                               (wrapper->pict expr)])
+                            where/sc)
+                       (cond
+                         [vertical-side-conditions? 
+                          ;; maximize line breaks:
+                          0]
+                         [compact-side-conditions?
+                          ;; maximize line break as needed:
+                          max-line-w/pre-sc]
+                         [else 
+                          ;; no line breaks:
+                          +inf.0]))])])))
   (case mode
     [(horizontal)
      (define (adjust-for-fills rows)
@@ -1000,47 +1043,60 @@
      (table 3
             (adjust-for-fills
              (apply append
-                    (map (lambda (lhs sc rhs linebreak?)
-                           (append
-                            (list
-                             (cond
-                               [linebreak?
-                                (list lhs 'fill 'fill)]
-                               [(and sc (eq? style 'left-right/beside-side-conditions))
-                                (list lhs =-pict (htl-append 10 rhs sc))]
-                               [else
-                                (list lhs =-pict rhs)]))
-                            (if linebreak?
-                                (list
-                                 (list (htl-append sep =-pict rhs)
-                                       'fill
-                                       'fill))
-                                null)
-                            (if (or (not sc)
-                                    (and (not linebreak?)
-                                         (eq? style 'left-right/beside-side-conditions)))
-                                null
-                                (list
-                                 (list sc 'fill 'fill)))))
-                         lhss
-                         scs
-                         rhss
-                         linebreak-list)))
+                    (for/list ([lhs/contract (in-list lhs/contracts)]
+                               [sc (in-list scs)]
+                               [rhs (in-list rhss)]
+                               [linebreak? (in-list linebreak-list)])
+                      (append
+                       (list
+                        (cond
+                          [(equal? rhs 'contract) ;; contract
+                           (list lhs/contract 'fill 'fill)]
+                          [linebreak?
+                           (list lhs/contract 'fill 'fill)]
+                          [(and sc (eq? style 'left-right/beside-side-conditions))
+                           (list lhs/contract =-pict (htl-append 10 rhs sc))]
+                          [else
+                           (list lhs/contract =-pict rhs)]))
+                       (if linebreak?
+                           (list
+                            (list (htl-append sep =-pict rhs)
+                                  'fill
+                                  'fill))
+                           null)
+                       (if (or (not sc)
+                               (and (not linebreak?)
+                                    (eq? style 'left-right/beside-side-conditions)))
+                           null
+                           (list
+                            (list sc 'fill 'fill)))))))
             ltl-superimpose ltl-superimpose
             sep sep)]
     [(vertical)
      (apply vl-append
             sep
             (apply append
-                   (map (lambda (lhs sc rhs)
-                          (cons
-                           (vl-append (htl-append lhs =-pict) rhs)
-                           (if (not sc)
-                               null
-                               (list sc))))
-                        lhss
-                        scs
-                        rhss)))]))
+                   (for/list ([lhs/contract (in-list lhs/contracts)]
+                              [sc (in-list scs)]
+                              [rhs (in-list rhss)])
+                     (cond
+                       [(equal? rhs 'contract) ;; contract
+                        (list lhs/contract)]
+                       [else
+                        (cons
+                         (vl-append (htl-append lhs/contract =-pict) rhs)
+                         (if (not sc)
+                             null
+                             (list sc)))]))))]))
+
+(define (render-metafunction-contract lang name doms rngs)
+  (hbl-append (basic-text (format "~a" name) (metafunction-style))
+              (basic-text " : " (default-style))
+              (apply hbl-append (add-between (map (λ (x) (lw->pict lang x)) doms) 
+                                             (basic-text " " (default-style))))
+              (basic-text " → " (default-style))
+              (apply hbl-append (add-between (map (λ (x) (lw->pict lang x)) rngs)
+                                             (basic-text " " (default-style))))))
 
 (define (metafunction-call name an-lw)
   (struct-copy lw an-lw
@@ -1122,14 +1178,14 @@
                                (basic-text "]" (default-style)))])]
     [else x]))
 
-(define (render-metafunction/proc mfs filename name)
+(define (render-metafunction/proc mfs contract? filename name)
   (cond
     [filename
-     (save-as-ps/pdf (λ () (metafunctions->pict/proc mfs name))
+     (save-as-ps/pdf (λ () (metafunctions->pict/proc mfs contract? name))
                      filename)]
     [else
      (parameterize ([dc-for-text-size (make-object bitmap-dc% (make-object bitmap% 1 1))])
-       (metafunctions->pict/proc mfs name))]))
+       (metafunctions->pict/proc mfs contract? name))]))
 
 (define (render-pict make-pict filename)
   (cond
diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/bitmap-test.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/bitmap-test.rkt
index ae04fa4bb9..471579655e 100644
--- a/pkgs/redex-pkgs/redex-test/redex/tests/bitmap-test.rkt
+++ b/pkgs/redex-pkgs/redex-test/redex/tests/bitmap-test.rkt
@@ -96,6 +96,7 @@
          "red-with-where-name.png"))
 
 (define-metafunction lang
+  S : x v e -> e
   [(S x v e) e])
 
 (btest (render-metafunction S)
diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/bmps-macosx/metafunctions-multiple.png b/pkgs/redex-pkgs/redex-test/redex/tests/bmps-macosx/metafunctions-multiple.png
index 977fe249b7..d3d3003993 100644
Binary files a/pkgs/redex-pkgs/redex-test/redex/tests/bmps-macosx/metafunctions-multiple.png and b/pkgs/redex-pkgs/redex-test/redex/tests/bmps-macosx/metafunctions-multiple.png differ