From 84fcd48039464024d0502014b9bdb4bf61a041b5 Mon Sep 17 00:00:00 2001 From: Jay McCarthy Date: Wed, 19 Mar 2014 15:16:00 -0600 Subject: [PATCH] stlc sub 2 --- .../redex-examples/redex/examples/benchmark/stlc-sub/2.diff | 4 ++++ .../redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt | 3 +++ 2 files changed, 7 insertions(+) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff index dc826fa6aa..4cfe9af64c 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff @@ -6,3 +6,7 @@ < (λ (x_new τ) (subst (replace M x_1 x_new) x_2 v)) --- > (λ (x_new τ) (subst (replace M x_new x_1) x_2 v)) +290a291,293 +> (define small-counter-example +> (term ((λ (x int) (λ (y int) y)) 1))) +> (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt index 98e1b8a2fa..74ca800935 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt @@ -288,3 +288,6 @@ (generate-term stlc M #:i-th index) (set! index (add1 index)))))) +(define small-counter-example + (term ((λ (x int) (λ (y int) y)) 1))) +(test-equal (check small-counter-example) #f)