Is this what you have in mind?
#lang racket
(require redex/reduction-semantics)
(define-language L
(ts ::= variable number))
(define-judgment-form L
#:mode (subsequence I I)
#:contract (subsequence (ts ...) (ts ...))
[----------------------------------------------
(subsequence (ts_1 ...)
(ts_2 ... ts_1 ... ts_3 ...))])
(test-judgment-holds
(subsequence () (1 2 3 4)))
(test-judgment-holds
(subsequence (1) (1 2 3 4)))
(test-judgment-holds
(subsequence (2) (1 2 3 4)))
(test-judgment-holds
(subsequence (1 2) (1 2 3 4)))
(test-judgment-holds
(subsequence (2 3) (1 2 3 4)))
(test-judgment-holds
(subsequence (3 4) (1 2 3 4)))
(test-judgment-holds
(subsequence (2 3 4) (1 2 3 4)))
(test-judgment-holds
(subsequence (1 2 3) (1 2 3 4)))
(test-judgment-holds
(subsequence (1 2 3 4) (1 2 3 4)))
(test-equal
(judgment-holds (subsequence (5) (1 2 3 4))) #f)
(test-equal
(judgment-holds (subsequence (3 2) (1 2 3 4))) #f)
(test-equal
(judgment-holds (subsequence (4 1) (1 2 3 4))) #f)
(test-results)
On Sat, Jan 30, 2021 at 11:46 AM Beatriz Moreira <beatriz.smore...@gmail.com>
wrote:
> Hi !
> I have a reduction relation where I have to match a pattern *ts* to two
> sequences, where the first one contains the other one. What I tried to do
> was something like this:
> 1st seq: (*ts_all1 ... ts ts_all2 ...*) 2nd seq: (*ts_x1 ... ts
> ts_x2 ...*), where *ts_x* *⊆ **ts_all*.
> But the problem is that with the pattern matching is that *ts_x1* doesn't
> match all elements of *ts_all1* .
> I'm trying to use side conditions but i can't seem to get it right :c .
> Any advice?
>
> Thank you , Beatriz :)
>
> --
> 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/1f9a3f57-787b-43b9-9fb4-560e425c1cdan%40googlegroups.com
> <https://groups.google.com/d/msgid/racket-users/1f9a3f57-787b-43b9-9fb4-560e425c1cdan%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/CAL3TdOMKZrDQ%2BUh0u9bVe6H2dzfS%3DcYDhx26yHSFCb3nzOpJTA%40mail.gmail.com.
