Condition within With and other scoping environments is disregarded

[aravindh-krishnamoorthy]

Description

Wolfram language reference for Condition states that a condition within the Module, Block, and With statements:

lhs:=Module[{vars},rhs/;test]

applies to the lhs, i.e., it's added as a condition to the lhs. Presently, the condition is not added to the lhs in Mathics. See also the additional qualification in Additional context.

How to Reproduce

Mathics:

In[4]:= Clear[f]
Out[4]= None
In[5]:= f[x_] := With[{}, x /; x != 0]
Out[5]= None
In[6]:= f[0]
Out[6]= 0 /; 0 ≠ 0

and Mathematica:

>> Clear[f];
>> f[x_] := With[{}, x /; x != 0]
>> f[0]
f[0]

Output Given

0 /; 0 ≠ 0

Expected behavior

f[0]

Your Environment

Mathics 7.0.1dev0
on CPython 3.11.10 | packaged by conda-forge | (main, Oct 16 2024, 01:27:36) [GCC 13.3.0]
using SymPy 1.13.3, mpmath 1.3.0, numpy 2.1.3, cython Not installed

Workarounds

This workaround returns Indeterminate when the condition is false. Also, it only works when Condition is the only statement within the With block. It's a bad hack, but works for Rubi for now.

Unprotect[With]; 
With[vars_, Verbatim[Condition][expr_, wcond_]] := Condition[With[vars, expr], With[vars, wcond]]; 
With[vars_, Verbatim[Condition][expr_, wcond_]] := Condition[Indeterminate, Not[With[vars, wcond]]]; 
Protect[With]; 

Priority

Medium; results in Indeterminate results when a rule is picked, but eventually the condition within With is false.

Additional context

Note that the condition is considered for lhs only if it's a part of the last statement, as shown below for Mathematica $14.1.0$.

>> Clear[x];
>> Clear[f];
>> f[x_] := With[{}, x /; x != 0; x + 1]
>> f[0]
1