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 <[email protected]>
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 [email protected].
> 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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/racket-users/CAL3TdOMKZrDQ%2BUh0u9bVe6H2dzfS%3DcYDhx26yHSFCb3nzOpJTA%40mail.gmail.com.
