I'm not sure without seeing more of your code (one annoying thing about Redex is that it is not always clear when you "in redex" and when you are "in racket" and your code might be mixing those up) but here is an example along the lines I think you're working towards. Note that it might be better to define in-dom as a judgment form (this would require you to define a metafunction that checks if two names are different) but I did it as a metafunction to show how that would work.
Robby #lang racket (require redex/reduction-semantics) (define-language L (e ::= (+ e e) x) (x y ::= variable-not-otherwise-mentioned) (Γ ::= · (x Γ))) (define-judgment-form L #:mode (closed-by I I) #:contract (closed-by Γ e) [(closed-by Γ e_1) (closed-by Γ e_2) ----------------------------------- (closed-by Γ (+ e_1 e_2))] [(side-condition (in-dom x Γ)) ----------------------------- (closed-by Γ x)]) (define-metafunction L in-dom : x Γ -> boolean [(in-dom x ·) #false] [(in-dom x (x Γ)) #true] [(in-dom x (y Γ)) (in-dom x Γ)]) (test-judgment-holds (closed-by (c ·) c)) (test-judgment-holds (closed-by (b (c ·)) b)) (test-judgment-holds (closed-by (b (c ·)) c)) (test-judgment-holds (closed-by (a (b (c ·))) (+ a (+ b c)))) (test-equal (judgment-holds (closed-by · a)) #false) (test-equal (judgment-holds (closed-by · (+ a (+ b c)))) #false) (test-results) On Thu, Jan 7, 2021 at 10:52 AM Beatriz Moreira <beatriz.smore...@gmail.com> wrote: > I have tried to use a metafunction to represent s∉dom(env-ß) in a side > condition,* (side-condition (notinenv ((ß_1 ...) env-ß ...) x))*, but > the error message *notinenv: illegal use of syntax in: (notinenv ((ß_1 > ...) env-ß ...) x) value at phase 1: #<term-fn>* appears and i don't > understand why. > > I defined *notinenv* as a simple metafunction just for testing: > (define-metafunction FS > notinenv : env-ß x -> any > [(notinenv (((x -> _) ß_1 ...) env-ß ...) x) #f] > [(notinenv ((ß_1 ...) env-ß ...) x) #t]) > > Thank you :) > > A segunda-feira, 21 de dezembro de 2020 à(s) 15:05:37 UTC, Robby Findler > escreveu: > >> I recommend you define a metafunction or judgment form that captures what >> you want exactly and then use that. >> >> Robby >> >> >> On Mon, Dec 21, 2020 at 8:32 AM Beatriz Moreira <beatriz....@gmail.com> >> wrote: >> >>> Hi, >>> I have been using side-condition to check if a sequence of variables >>> exist is in an environment , like this : >>> >>> *(side-condition (not (member (term ((s : _) ...)) (term (env-ß_1 >>> ...)))))* >>> >>> being s a state variable and _ a value that i don't know. But it doesn't >>> seem to work as expected, as it returns #t even when it shouldn't. >>> Is it there a better way of doing it? >>> >>> Thank you :) >>> >>> -- >>> You received this message because you are subscribed to the Google >>> Groups "Racket Users" group. >>> To unsubscribe from this group and stop receiving emails from it, send >>> an email to racket-users...@googlegroups.com. >>> To view this discussion on the web visit >>> https://groups.google.com/d/msgid/racket-users/c8632f31-98c2-46cb-8231-2ca272ae2b8an%40googlegroups.com >>> <https://groups.google.com/d/msgid/racket-users/c8632f31-98c2-46cb-8231-2ca272ae2b8an%40googlegroups.com?utm_medium=email&utm_source=footer> >>> . >>> >> -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to racket-users+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/racket-users/30754357-0563-4709-8d88-f0f8ef5d8b63n%40googlegroups.com > <https://groups.google.com/d/msgid/racket-users/30754357-0563-4709-8d88-f0f8ef5d8b63n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAL3TdOOjKuczdg0S6XhHeCi9QuJRtFLb8EBOUzQWVqhJfbsyCQ%40mail.gmail.com.
