use hyphens in the example define-judgment-forms for STLC

pkgs/redex-pkgs/redex-examples/redex/examples/define-judgment-form/typing-rules-no-ellipses.rkt

@@ -27,15 +27,25 @@
 (define-judgment-form STLC
   #:mode (typeof I I O)
   #:contract (typeof Γ e τ)
-  [(typeof Γ (λ (x τ_1) e) (τ_1 → τ_2))
+  
-   (typeof ([x τ_1] Γ) e τ_2)]
+  [(typeof ([x τ_1] Γ) e τ_2)
-  [(typeof Γ (e_1 e_2) τ)
+   ------------------------------------
-   (typeof Γ e_1 (τ_2 → τ))
+   (typeof Γ (λ (x τ_1) e) (τ_1 → τ_2))]
-   (typeof Γ e_2 τ_2)]
+  
-  [(typeof Γ x τ)
+  [(typeof Γ e_1 (τ_2 → τ))
-   (where τ (lookup Γ x))]
+   (typeof Γ e_2 τ_2)
-  [(typeof Γ i int)]
+   ------------------------
-  [(typeof Γ add1 (int → int))])
+   (typeof Γ (e_1 e_2) τ)]
+  
+  [(where τ (lookup Γ x))
+   --------------
+   (typeof Γ x τ)]
+  
+  [----------------
+   (typeof Γ i int)]
+  
+  [---------------------------
+   (typeof Γ add1 (int → int))])
 
 
 (define-metafunction STLC

pkgs/redex-pkgs/redex-examples/redex/examples/define-judgment-form/typing-rules.rkt

@@ -35,15 +35,25 @@
 (define-judgment-form STLC
   #:mode (typeof I I O)
   #:contract (typeof Γ e τ)
-  [(typeof Γ (λ (x τ_1) e) (τ_1 → τ_2))
+  
-   (typeof (extend Γ x τ_1) e τ_2)]
+  [(typeof (extend Γ x τ_1) e τ_2)
-  [(typeof Γ (e_1 e_2) τ)
+   ------------------------------------
-   (typeof Γ e_1 (τ_2 → τ))
+   (typeof Γ (λ (x τ_1) e) (τ_1 → τ_2))]
-   (typeof Γ e_2 τ_2)]
+  
-  [(typeof Γ x τ)
+  [(typeof Γ e_1 (τ_2 → τ))
-   (where τ (lookup Γ x))]
+   (typeof Γ e_2 τ_2)
-  [(typeof Γ i int)]
+   ------------------------
-  [(typeof Γ add1 (int → int))])
+   (typeof Γ (e_1 e_2) τ)]
+  
+  [(where τ (lookup Γ x))
+   --------------
+   (typeof Γ x τ)]
+  
+  [----------------
+   (typeof Γ i int)]
+  
+  [----------------------------
+   (typeof Γ add1 (int → int))])
 
 (define-metafunction STLC
   extend : Γ x τ -> Γ