Assuming

Evaluate $expr$ with $cond$ assumed for the duration of the call, then forget it. Provided by @enumeratio/analytic.

✓ checked against that system · ! checked, with disagreements (hover a chip)Wolfram LanguageAssuming!↗

Assuming(cond, expr)evaluate $expr$ under a single assumed condition, a List of them (an implicit conjunction), or an And of them.

Typed signatures

Type	Package	Applies
(expression, expression) -> expression	analytic	always

Domain: Analytic

Details

• Built on compute-engine's own assumption store: the condition is pushed in a fresh scope (ce.pushScope/ce.assume), $expr$ is evaluated, and the scope is popped — compute-engine documents assumptions as scoped, so popping restores exactly what was in force before, even nested and even mid-evaluation (unlike ce.checkpoint, which refuses there).
• No leakage: an assumption made here is gone once the call returns, whatever $expr$ does — verified by asking about the assumed symbol immediately after.
• What resolves under the assumption is whatever compute-engine's own evaluate() already consults assumptions for — Abs, Sign, and $\ln \circ \exp$ among them. This is more eager than bare Wolfram evaluation for those heads (Wolfram leaves Abs(x) alone until Refine/Simplify names it explicitly); it is not a general Simplify.

Examples

Basic #

$|x| = x$ once $x > 0$ is assumed

live ↗

In$\mathrm{Assuming}(x\gt0, \vert x\vert)$Out$x$

a List of conditions is an implicit conjunction: $\operatorname{sign}(x) + \operatorname{sign}(y) = 0$ under $x>0 \wedge y<0$

live ↗

In$\mathrm{Assuming}(\begin{cases}x\gt0\\y\lt0\end{cases}, \mathrm{sgn}(x)+\mathrm{sgn}(y))$Out$0$

live ↗

In$\mathrm{Assuming}(a\gt0, \bigl\lbrack\mathrm{Refine}(\sqrt{a^2}), \int_{0}^{1}\!x^{a}\, \mathrm{d}x\bigr\rbrack)$Out$\bigl\lbrack a, \frac{1}{a+1}\bigr\rbrack$

live ↗

In$\mathrm{Assuming}(x≥0∧y\lt0, \text{if }\mathrm{IsTrue}(\mathrm{Refine}(x-y\gt0))\text{ then }\mathrm{Refine}(\sqrt{x^2y^2})\text{ else }0)$Out$-(xy)$

Scope #

Wraps an expression in assumptions and leaves the body as is

live ↗

In$\mathrm{Assuming}(n∈ℤ∧p∈\mathbb{P}∧n\gt0, \mathrm{operations})$Out$\mathrm{operations}$

live ↗

In$\mathrm{Assuming}(a\gt0, \bigl\lbrack\int_{0}^{1}\!\frac{1}{x+a}\, \mathrm{d}x, \mathrm{FourierTransform}(\frac{1}{x^2+a}, x, w)\bigr\rbrack)$Out$\bigl\lbrack\ln(a+1)-\ln(a), \mathrm{FourierTransform}(\frac{1}{x^2+a}, x, w)\bigr\rbrack$

Properties #

the assumption on $z$ is gone as soon as Assuming returns — the second $\operatorname{sign}(z)$ stays symbolic

live ↗

In$\bigl\lbrack\mathrm{Assuming}(z\gt0, \mathrm{sgn}(z)), \mathrm{sgn}(z)\bigr\rbrack$Out$\bigl\lbrack1, \mathrm{sgn}(z)\bigr\rbrack$

Nested assumptions let the square root simplify, giving $-xy$

live ↗

In$\mathrm{Assuming}(x≥0, \mathrm{Assuming}(y\lt0, \mathrm{Refine}(\sqrt{x^2y^2})))$Out$-(xy)$

live ↗

In$\mathrm{Assuming}(m\bmod2=0, \mathrm{Simplify}(\cos(kπ)^{m}, k∈ℤ))$Out$((-1)^{k})^{m}$

About

Examples	9
Checked against	Wolfram Language 7 agree1 differ1 unevaluated
Crosswalk	Wolfram Language

Implementation

mappedwolframpackages/oracle/src/mappings.ts

Wolfram's own Assuming only affects functions that consult $Assumptions (Simplify, FullSimplify, Refine) — a bare Abs(x) inside it stays symbolic, unlike compute-engine's own eager assumption-aware evaluate(). Wrapping the body in FullSimplify is what makes the oracle check the same claim we do.