gistfile1.scm

  (define λcon-rr
    (reduction-relation
     λcon
     (D (aop i_1 i_2)
        (δ (aop i_1 i_2))
        δ)
     (D (rop i_1 i_2)
        (compare (rop i_1 i_2))
        compare)
     (D (string? v)
        (is-string? (string? v))
        is-string?)
...
     with
     [(--> (in-hole E M) (in-hole E N)) (D M N)]))

(define λcon-g-rr
    (extend-reduction-relation 
     λcon-rr
     λcon-g
     (--> ((in-hole E (check v e)) || φ)
          ((in-hole E e) || φ)
          check)
     (--> ((in-hole E (output v_1 e)) || (v_2 ...))
          ((in-hole E e) || (v_1 v_2 ...))
          output)
     with
     [(--> ((in-hole E e_a) || φ)
           ((in-hole E e_b) || φ))
      (D a b)]
     [(--> ((in-hole E e) || φ)
           ((error str) || φ))
      (D e (error str))]))