test.rkt

#lang racket/base

(require
 redex/reduction-semantics)

(define-language stlc
  [t ::= nat (-> t t)]
  [e m ::= natural x (λ (x : t) e) (e e)]
  [x ::= variable-not-otherwise-mentioned]
  [Γ ::= ∅ (Γ x : t)]
  #:binding-forms
  (λ (x : t) e #:refers-to x))

(define-metafunction stlc
  Γ-in-dom : Γ x -> #t or #f
  [(Γ-in-dom ∅ x)
   #f]
  [(Γ-in-dom (Γ x : t) x)
   #t]
  [(Γ-in-dom (Γ x_!_0 : t) (name x x_!_0))
   (Γ-in-dom x)])

(define-metafunction stlc
  Γ-ref : Γ x -> t
  #:pre (Γ-in-dom Γ x)
  [(Γ-ref (Γ x : t) x)
   t]
  [(Γ-ref (Γ x_!_0 : t) (name x x_!_0))
   (Γ-ref Γ x)])

(define-metafunction stlc
  Γ-ref_0 : Γ_0 x_0 -> t
  #:pre (Γ-in-dom Γ_0 x_0)
  [(Γ-ref_0 (Γ x : t) x)
   t]
  [(Γ-ref_0 (Γ x_!_0 : t) (name x x_!_0))
   (Γ-ref_0 Γ x)])

(module+ test
  (test-equal
   (term (Γ-ref_0 (∅ x : nat) x))
   (term nat))
  (test-equal
   (term (Γ-ref (∅ x : nat) x))
   (term nat)))