suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

stlc sub 4

Browse Source
This commit is contained in:
Jay McCarthy 2014-03-19 15:34:26 -06:00
parent b1bc4ce430
commit 00988db325
2 changed files with 17 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/4.diff
View File

@ -6,3 +6,12 @@
< (where x_new ,(variable-not-in (term (x_1 e x_2)) < (where x_new ,(variable-not-in (term (x_1 e x_2))
--- ---
> (where x_new ,(variable-not-in (term e) > (where x_new ,(variable-not-in (term e)
290a291,298
> (define small-counter-example
> ;; XXX I don't think this actually has an error because if x_1 !=
> ;; x_2 and v is a closed term, then what could go wrong? If we
> ;; remove the other special case of subst for λs that match, then it
> ;; would be bad, though.
> (term ((λ (x int) (λ (y int) (λ (y int) ((+ x) y))))
> 1)))
> (test-equal (check small-counter-example) #f)

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt
View File

@ -288,3 +288,11 @@
(generate-term stlc M #:i-th index) (generate-term stlc M #:i-th index)
(set! index (add1 index)))))) (set! index (add1 index))))))
(define small-counter-example
;; XXX I don't think this actually has an error because if x_1 !=
;; x_2 and v is a closed term, then what could go wrong? If we
;; remove the other special case of subst for λs that match, then it
;; would be bad, though.
(term ((λ (x int) (λ (y int) (λ (y int) ((+ x) y))))
1)))
(test-equal (check small-counter-example) #f)