Right, so I need a separate metafunction for each pattern I want to negate.
On Mon, Oct 24, 2016 at 6:56 PM, Robby Findler
wrote:
> I am saying to write this:
>
> (define-metafunction L
> [(not-thing pat) #false]
> [(not-thing any) #true])
>
> and then where you wrote:
>
> (where/not pat t
I am saying to write this:
(define-metafunction L
[(not-thing pat) #false]
[(not-thing any) #true])
and then where you wrote:
(where/not pat tm)
write this:
(where #true (not-thing pat))
On Mon, Oct 24, 2016 at 5:47 PM, Sam Caldwell wrote:
>> In the meantime, consider using a metaf
> In the meantime, consider using a metafunction with an `else` clause.
This would entail fixing the pattern, right? As in, I can write a
metafunction deciding whether a term does not match a pattern, but I can't
write a metafunction taking both the term and the pattern.
I'm ok with failed matche
Unfortunately, Redex's pattern language does not currently support
`not`. It might be easy to add it, or maybe hard, or maybe impossible.
Offhand, it seems probably possible to support in the unifier and
impossible in the enumerator and not hard in the matcher.
In the meantime, consider using a me
I have a Redex judgment that I would like to specify in terms of a *failed*
pattern match. I can write this like so:
[(side-condition ,(not (redex-match? L pat (term tm)))
--
...]
which works, but I would rather just abbreviate this
5 matches
Mail list logo
