Add documentation about literal terms

Author: leafac

redex-doc/redex/scribblings/ref/terms.scrbl

@@ -29,8 +29,7 @@ stands for repetition unless otherwise indicated):
          (in-hole term term)
          hole
          (mf-apply identifier term ...)
-         #t #f
-         string]
+         literal]
    [term-sequence 
      term
      ,@expr
@@ -64,8 +63,15 @@ them.}
 @item{A term written @racket[(mf-apply f arg ...)] asserts that @racket[f]
 is a @tech{metafunction} and produces the term @racket[(f arg ...)].}
 
-@item{A term written as a literal boolean or a string
-produces the boolean or the string.}
+ @item{A term written as a literal produces that literal.
+  Term substitution and metafunction application do not occur
+  within literal values. For example,
+
+  @racketblock[
+ (term-let ([a 1]) (term #hash((x . a))))
+ ]
+
+ Evaluates to @racket['#hash((x . a))], not @racket['#hash((x . 1))].}
 ]
 
 @defform*[[(term @#,tttterm) (term @#,tttterm #:lang lang-id)]]{

redex-test/redex/tests/term-test.rkt

@@ -13,6 +13,10 @@
 (test (term (1 ,(+ 1 1))) (list 1 2))
 (test (term-let ([x 1]) (term (x x))) (list 1 1))
 (test (term-let ([(x ...) (list 1 2 3)]) (term ((y x) ...))) '((y 1) (y 2) (y 3)))
+(test (term #hash((a . 2))) #hash((a . 2)))
+(test (term-let ([x 1]) #hash((a . x))) #hash((a . x)))
+(test (term #s(a 2 3 4)) #s(a 2 3 4))
+(test (term-let ([x 1]) #s(a 2 x 4)) #s(a 2 x 4))
 
 (test (term (in-hole (1 hole) 2)) (term (1 2)))
 (test (term (in-hole (1 hole (hole x)) 2)) (term (1 2 (hole x))))