tutorial. 用miniKanren查询数学规则[math-0009]

数学规则不是散落在文章里的字符串清单。Grove把规则以关系形式公开，因此文章可以查询名字、类别、适用模式和docstring。此处的输出由构建时查询生成。

一次查询得到所有规则元数据[#119]

共查询到78条规则。每一行依次含有名称、类别、适用模式以及可选说明：

((curl-curl-identity vector-calculus (forward backward check) "Replace the curl of a curl by the gradient of the divergence minus the vector Laplacian. The field must be C2; declaring it divergence-free is a separate premise and a separate rewrite.") (divergence-free vector-calculus (forward backward check) #f) (div-curl-zero vector-calculus (forward backward check) #f) (curl-grad-zero vector-calculus (forward backward check) #f))

这个format仅把前四个关系结果转成可读Scheme数据供本页展示；它不参与规则执行。完整规则名称会由下面的查询渲染。

关系约束可以筛选结果[#120]

下面查询微分规则：

((differentiate-constant (forward check) #f) (differentiate-variable (forward check) #f) (differentiate-independent (forward check) #f) (differentiate-negation (forward check) #f) (differentiate-sum (forward check) #f) (differentiate-difference (forward check) #f) (differentiate-product (forward check) "Generate the derivative of each factor separately and sum the two products. This rule constructs derivative terms; subsequent differentiation and simplification steps compute and reduce them.") (differentiate-power (forward check) #f) (differentiate-quotient (forward check) "Apply the quotient rule on the domain where the denominator is nonzero. The derivative remains a symbolic term until later passes process its operands and simplify the result.") (differentiate-sin (forward check) #f) (differentiate-cos (forward check) #f) (differentiate-exp (forward check) #f) (differentiate-log (forward check) #f) (differentiate-function (forward check) "Apply the shared function chain rule using one-based argument positions. C1 permits one derivative, C2 permits two, and smooth permits higher derivatives."))

ruleo描述规则目录中的事实；query声明要返回哪些逻辑变量；把类别固定为differentiate会只返回匹配的规则。关系可以进一步组合，而不需要手写列表过滤代码。

查询空间和分量规则：

((components-sum components (forward check) #f) (components-difference components (forward check) #f) (components-negation components (forward check) #f) (components-scale-left components (forward check) #f) (components-scale-right components (forward check) #f) (components-quotient components (forward check) #f) (components-dot components (forward check) #f) (components-cross components (forward check) #f) (components-zero components (forward check) #f) (gradient-components spatial (forward check) #f) (divergence-components spatial (forward check) #f) (curl-components spatial (forward check) #f) (laplacian-scalar-components spatial (forward check) #f) (laplacian-vector-components spatial (forward check) #f))

run*收集满足目标的所有解；conde表示两种可接受类别；==统一类别变量与符号。以上目标只是在规则目录上查询，尚未对某个表达式运行计算。

让规则说明从docstring自动生成[#121]

curl-curl-identity

Replace the curl of a curl by the gradient of the divergence minus the vector Laplacian. The field must be C2; declaring it divergence-free is a separate premise and a separate rewrite.

\frac{c2 (field) field : vector}{\nabla \times (\nabla \times field) \to \nabla (\nabla \cdot field) - Δ field} [curl-curl-identity]

Group: vector-calculus. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: assumptions declare vector(E) and c2(E)

Exact scalar-algebra check: unsupported.

divergence-free

\frac{\nabla \cdot field = 0 field : vector}{\nabla (\nabla \cdot field) \to \vec{0}} [divergence-free]

Group: vector-calculus. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: vector(E) and the matching fact div(E) = 0

Exact scalar-algebra check: unsupported.

div-curl-zero

\frac{c2 (field) field : vector}{\nabla \cdot (\nabla \times field) \to 0} [div-curl-zero]

Group: vector-calculus. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: assumptions declare vector(E) and c2(E)

Exact scalar-algebra check: unsupported.

curl-grad-zero

\frac{c2 (field) field : scalar}{\nabla \times (\nabla field) \to \vec{0}} [curl-grad-zero]

Group: vector-calculus. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: assumptions declare scalar(f) and c2(f)

Exact scalar-algebra check: unsupported.

div-grad-laplacian

\frac{c2 (field) field : scalar}{\nabla \cdot (\nabla field) \to Δ field} [div-grad-laplacian]

Group: vector-calculus. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: assumptions declare scalar(f) and c2(f)

Exact scalar-algebra check: unsupported.

grad-product

Differentiate the product of two scalar fields with the gradient product rule. C1 regularity suffices; no second derivatives or smoothness assumptions are required.

\frac{differentiable (f) differentiable (g) f : scalar g : scalar}{\nabla (f \times g) \to g \times \nabla f + f \times \nabla g} [grad-product]

Group: vector-calculus. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: scalar C1 fields in Cartesian space

Exact scalar-algebra check: unsupported.

div-product

\frac{differentiable (f) differentiable (e) f : scalar e : vector}{\nabla \cdot (f \times e) \to \nabla f \cdot e + f \times \nabla \cdot e} [div-product]

Group: vector-calculus. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: scalar and vector C1 fields in Cartesian space

Exact scalar-algebra check: unsupported.

curl-product

Expand the curl of a scalar times a vector field in oriented Cartesian space. The cross product is grad(f) cross E, in that order; reversing it changes the sign. Both factors need C1 regularity.

\frac{differentiable (f) differentiable (e) f : scalar e : vector}{\nabla \times (f \times e) \to \nabla f \times e + f \times \nabla \times e} [curl-product]

Group: vector-calculus. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: scalar and vector C1 fields in oriented Cartesian space

Exact scalar-algebra check: unsupported.

subtract-zero

\frac{(math-typeo facts term type); executable guards apply}{zero - term \to - term} [subtract-zero]

Group: identity. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: matching scalar or vector types

Exact scalar-algebra check: semantically-checked.

Executable guards

((zeroo type zero))

add-zero

\frac{(math-typeo facts term type); executable guards apply}{term + zero \to term} [add-zero]

Group: identity. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: matching scalar or vector types

Exact scalar-algebra check: semantically-checked.

Executable guards

((zeroo type zero))

zero-add

\frac{(math-typeo facts term type); executable guards apply}{zero + term \to term} [zero-add]

Group: identity. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: matching scalar or vector types

Exact scalar-algebra check: semantically-checked.

Executable guards

((zeroo type zero))

subtract-right-zero

\frac{(math-typeo facts term type); executable guards apply}{term - zero \to term} [subtract-right-zero]

Group: identity. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: matching scalar or vector types

Exact scalar-algebra check: semantically-checked.

Executable guards

((zeroo type zero))

double-negation

\frac{(math-typeo facts term type); executable guards apply}{- (- term) \to term} [double-negation]

Group: identity. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: X is scalar or vector

Exact scalar-algebra check: semantically-checked.

Executable guards

((conde ((== type (quote scalar))) ((== type (quote vector)))))

multiply-one

\frac{(math-typeo facts term type); executable guards apply}{term \times 1 \to term} [multiply-one]

Group: identity. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: X is scalar or vector

Exact scalar-algebra check: semantically-checked.

Executable guards

((conde ((== type (quote scalar))) ((== type (quote vector)))))

one-multiply

\frac{(math-typeo facts term type); executable guards apply}{1 term \to term} [one-multiply]

Group: identity. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: X is scalar or vector

Exact scalar-algebra check: semantically-checked.

Executable guards

((conde ((== type (quote scalar))) ((== type (quote vector)))))

multiply-zero

\frac{term : scalar}{term \times 0 \to 0} [multiply-zero]

Group: identity. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: X is scalar

Exact scalar-algebra check: semantically-checked.

zero-multiply

\frac{term : scalar}{0 term \to 0} [zero-multiply]

Group: identity. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: X is scalar

Exact scalar-algebra check: semantically-checked.

power-one

\frac{term : scalar}{{term}^{1} \to term} [power-one]

Group: identity. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: X is scalar

Exact scalar-algebra check: semantically-checked.

power-zero

\frac{term : scalar}{{term}^{0} \to 1} [power-zero]

Group: identity. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: polynomial power convention

Exact scalar-algebra check: semantically-checked.

add-commutative

\frac{left : scalar right : scalar}{left + right \to right + left} [add-commutative]

Group: polynomial-algebra. Modes: (check). Declarative RuleSpec; metavariables denote terms. Condition: scalar terms

Exact scalar-algebra check: semantically-checked.

multiply-associative

\frac{left : scalar middle : scalar right : scalar}{left \times middle \times right \to left \times middle \times right} [multiply-associative]

Group: polynomial-algebra. Modes: (check). Declarative RuleSpec; metavariables denote terms. Condition: scalar terms

Exact scalar-algebra check: semantically-checked.

add-associative

\frac{left : scalar middle : scalar right : scalar}{left + middle + right \to left + middle + right} [add-associative]

Group: polynomial-algebra. Modes: (check). Declarative RuleSpec; metavariables denote terms. Condition: scalar terms

Exact scalar-algebra check: semantically-checked.

multiply-commutative

\frac{left : scalar right : scalar}{left \times right \to right \times left} [multiply-commutative]

Group: polynomial-algebra. Modes: (check). Declarative RuleSpec; metavariables denote terms. Condition: scalar terms

Exact scalar-algebra check: semantically-checked.

differentiate-constant

\frac{(unquote (quasiquote (unquote expression))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (expression) \to 0} [differentiate-constant]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts expression coordinate) (if (differentiable-term? (quasiquote (unquote expression)) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (project (expression) (if (math-number-value expression) succeed fail)))

differentiate-variable

\frac{(unquote (quasiquote (var (unquote coordinate)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (coordinate) \to 1} [differentiate-variable]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts coordinate) (if (differentiable-term? (quasiquote (var (unquote coordinate))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

differentiate-independent

\frac{(unquote (quasiquote (var (unquote other)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (other) \to 0} [differentiate-independent]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts other coordinate) (if (differentiable-term? (quasiquote (var (unquote other))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (=/= other coordinate))

differentiate-negation

\frac{(unquote (quasiquote (- (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (- operand) \to - (\frac{d}{d coordinate} (operand))} [differentiate-negation]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (- (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

differentiate-sum

\frac{(unquote (quasiquote (+ (unquote left) (unquote right)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (left + right) \to \frac{d}{d coordinate} (left) + \frac{d}{d coordinate} (right)} [differentiate-sum]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts left right coordinate) (if (differentiable-term? (quasiquote (+ (unquote left) (unquote right))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

differentiate-difference

\frac{(unquote (quasiquote (- (unquote left) (unquote right)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (left - right) \to \frac{d}{d coordinate} (left) - \frac{d}{d coordinate} (right)} [differentiate-difference]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts left right coordinate) (if (differentiable-term? (quasiquote (- (unquote left) (unquote right))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

differentiate-product

Generate the derivative of each factor separately and sum the two products. This rule constructs derivative terms; subsequent differentiation and simplification steps compute and reduce them.

\frac{(unquote (quasiquote (* (unquote left) (unquote right)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (left \times right) \to \frac{d}{d coordinate} (left) \times right + left \times \frac{d}{d coordinate} (right)} [differentiate-product]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts left right coordinate) (if (differentiable-term? (quasiquote (* (unquote left) (unquote right))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

differentiate-power

\frac{(unquote (quasiquote (^ (unquote base) (num (unquote exponent))))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} ({base}^{exponent}) \to result} [differentiate-power]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts base exponent result coordinate) (if (differentiable-term? (quasiquote (^ (unquote base) (num (unquote exponent)))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (project (exponent base coordinate) (let ((n (natural-value exponent))) (if (= n 0) (== result (quote (num "0"))) (== result (quasiquote (* (* (num (unquote exponent)) (^ (unquote base) (num (unquote (number->string (- n 1)))))) (differentiate (unquote base) (var (unquote coordinate))))))))))

differentiate-quotient

Apply the quotient rule on the domain where the denominator is nonzero. The derivative remains a symbolic term until later passes process its operands and simplify the result.

\frac{(unquote (quasiquote (/ (unquote left) (unquote right)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (\frac{left}{right}) \to \frac{\frac{d}{d coordinate} (left) \times right - left \times \frac{d}{d coordinate} (right)}{{right}^{2}}} [differentiate-quotient]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts left right coordinate) (if (differentiable-term? (quasiquote (/ (unquote left) (unquote right))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (math-factso facts (quasiquote ((nonzero (unquote right))))))

differentiate-sin

\frac{(unquote (quasiquote (sin (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (\sin (operand)) \to \frac{d}{d coordinate} (operand) \times \cos (operand)} [differentiate-sin]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (sin (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

differentiate-cos

\frac{(unquote (quasiquote (cos (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (\cos (operand)) \to - (\frac{d}{d coordinate} (operand) \times \sin (operand))} [differentiate-cos]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (cos (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

differentiate-exp

\frac{(unquote (quasiquote (exp (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (\exp (operand)) \to \frac{d}{d coordinate} (operand) \times \exp (operand)} [differentiate-exp]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (exp (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

differentiate-log

\frac{(unquote (quasiquote (log (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (\log (operand)) \to \frac{\frac{d}{d coordinate} (operand)}{operand}} [differentiate-log]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (log (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (math-factso facts (quasiquote ((positive (unquote operand))))))

differentiate-function

Apply the shared function chain rule using one-based argument positions. C1 permits one derivative, C2 permits two, and smooth permits higher derivatives.

\frac{Declared scalar function and sufficient regularity for the next derivative; algorithm applicability checked}{Derivative of f(u_1,...,u_n) = sum_i partial_i f(u_1,...,u_n) derivative of u_i} [differentiate-function]

Group: differentiate. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: Declared scalar function and sufficient regularity for the next derivative

Exact scalar-algebra check: unsupported.

evaluate-constant

\frac{exact scalar arithmetic; algorithm applicability checked}{exact constant arithmetic} [evaluate-constant]

Group: calculate. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: exact scalar arithmetic

Exact scalar-algebra check: unsupported.

collect-like-terms

\frac{exact scalar arithmetic; algorithm applicability checked}{a*X + b*X = (a+b)*X} [collect-like-terms]

Group: collect. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: exact scalar arithmetic

Exact scalar-algebra check: unsupported.

combine-coefficients

\frac{exact scalar arithmetic; algorithm applicability checked}{a*(b*X) = (a*b)*X} [combine-coefficients]

Group: collect. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: exact scalar arithmetic

Exact scalar-algebra check: unsupported.

normalize-scalar

\frac{real scalar algebra; algorithm applicability checked}{normalize-scalar} [normalize-scalar]

Group: normalize. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: real scalar algebra

Exact scalar-algebra check: unsupported.

cancel-scalar-factors

\frac{real scalar algebra; algorithm applicability checked}{cancel-scalar-factors} [cancel-scalar-factors]

Group: cancel. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: real scalar algebra

Exact scalar-algebra check: unsupported.

cancel-common-factor

A check-only cancellation theorem. Its denominator side condition is explicit in the premise and must remain in the surrounding domain requirements.

\frac{nonzero (factor) value : scalar factor : scalar}{\frac{value \times factor}{factor} \to value} [cancel-common-factor]

Group: cancel. Modes: (check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar terms; A is nonzero

Exact scalar-algebra check: semantically-checked.

expand-scalar-product

\frac{real scalar algebra; algorithm applicability checked}{expand-scalar-product} [expand-scalar-product]

Group: expand. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: real scalar algebra

Exact scalar-algebra check: unsupported.

normalize-function-prime

\frac{differentiable (name) (unquote (quasiquote (prime (var (unquote name)) (unquote argument)))) : scalar}{{name}^{'} (argument) \to (darg ((unquote name) (unquote argument)) (num "1"))} [normalize-function-prime]

Group: normalize. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Declared unary scalar function with one derivative

Exact scalar-algebra check: unsupported.

partial-constant

\frac{coordinate (coordinate) differentiable (expression) (unquote (quasiquote (unquote expression))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (expression) \to 0} [partial-constant]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts expression coordinate) (if (differentiable-term? (quasiquote (unquote expression)) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (project (expression) (if (math-number-value expression) succeed fail)))

partial-variable

\frac{coordinate (coordinate) differentiable (coordinate) (unquote (quasiquote (var (unquote coordinate)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (coordinate) \to 1} [partial-variable]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts coordinate) (if (differentiable-term? (quasiquote (var (unquote coordinate))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

partial-independent

\frac{coordinate (coordinate) differentiable (other) (unquote (quasiquote (var (unquote other)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (other) \to 0} [partial-independent]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts other coordinate) (if (differentiable-term? (quasiquote (var (unquote other))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (=/= other coordinate) (project (facts input) (if (independent-variable? facts input) succeed fail)))

partial-negation

\frac{coordinate (coordinate) differentiable (- operand) (unquote (quasiquote (- (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (- operand) \to - (\frac{\partial}{\partial coordinate} (operand))} [partial-negation]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (- (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

partial-sum

\frac{coordinate (coordinate) differentiable (left + right) (unquote (quasiquote (+ (unquote left) (unquote right)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (left + right) \to \frac{\partial}{\partial coordinate} (left) + \frac{\partial}{\partial coordinate} (right)} [partial-sum]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts left right coordinate) (if (differentiable-term? (quasiquote (+ (unquote left) (unquote right))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

partial-difference

\frac{coordinate (coordinate) differentiable (left - right) (unquote (quasiquote (- (unquote left) (unquote right)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (left - right) \to \frac{\partial}{\partial coordinate} (left) - \frac{\partial}{\partial coordinate} (right)} [partial-difference]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts left right coordinate) (if (differentiable-term? (quasiquote (- (unquote left) (unquote right))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

partial-product

\frac{coordinate (coordinate) differentiable (left \times right) (unquote (quasiquote (* (unquote left) (unquote right)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (left \times right) \to \frac{\partial}{\partial coordinate} (left) \times right + left \times \frac{\partial}{\partial coordinate} (right)} [partial-product]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts left right coordinate) (if (differentiable-term? (quasiquote (* (unquote left) (unquote right))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

partial-power

\frac{coordinate (coordinate) differentiable ({base}^{exponent}) (unquote (quasiquote (^ (unquote base) (num (unquote exponent))))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} ({base}^{exponent}) \to result} [partial-power]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts base exponent result coordinate) (if (differentiable-term? (quasiquote (^ (unquote base) (num (unquote exponent)))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (project (exponent base coordinate) (let ((n (natural-value exponent))) (if (= n 0) (== result (quote (num "0"))) (== result (quasiquote (* (* (num (unquote exponent)) (^ (unquote base) (num (unquote (number->string (- n 1)))))) (partial (unquote base) (var (unquote coordinate))))))))))

partial-quotient

\frac{coordinate (coordinate) differentiable (\frac{left}{right}) (unquote (quasiquote (/ (unquote left) (unquote right)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (\frac{left}{right}) \to \frac{\frac{\partial}{\partial coordinate} (left) \times right - left \times \frac{\partial}{\partial coordinate} (right)}{{right}^{2}}} [partial-quotient]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts left right coordinate) (if (differentiable-term? (quasiquote (/ (unquote left) (unquote right))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (math-factso facts (quasiquote ((nonzero (unquote right))))))

partial-sin

\frac{coordinate (coordinate) differentiable (\sin (operand)) (unquote (quasiquote (sin (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (\sin (operand)) \to \frac{\partial}{\partial coordinate} (operand) \times \cos (operand)} [partial-sin]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (sin (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

partial-cos

\frac{coordinate (coordinate) differentiable (\cos (operand)) (unquote (quasiquote (cos (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (\cos (operand)) \to - (\frac{\partial}{\partial coordinate} (operand) \times \sin (operand))} [partial-cos]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (cos (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

partial-exp

\frac{coordinate (coordinate) differentiable (\exp (operand)) (unquote (quasiquote (exp (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (\exp (operand)) \to \frac{\partial}{\partial coordinate} (operand) \times \exp (operand)} [partial-exp]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (exp (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

partial-log

\frac{coordinate (coordinate) differentiable (\log (operand)) (unquote (quasiquote (log (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (\log (operand)) \to \frac{\frac{\partial}{\partial coordinate} (operand)}{operand}} [partial-log]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (log (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (math-factso facts (quasiquote ((positive (unquote operand))))))

partial-function-chain

Apply the shared function chain rule using one-based argument positions. C1 permits one derivative, C2 permits two, and smooth permits higher derivatives.

\frac{Declared scalar function and sufficient regularity for the next derivative; algorithm applicability checked}{Derivative of f(u_1,...,u_n) = sum_i partial_i f(u_1,...,u_n) derivative of u_i} [partial-function-chain]

Group: partial. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: Declared scalar function and sufficient regularity for the next derivative

Exact scalar-algebra check: unsupported.

partial-coordinate-symmetry

\frac{C2 operand; coordinate names and argument positions have separate orders; algorithm applicability checked}{Exchange mixed derivatives into ascending order} [partial-coordinate-symmetry]

Group: normalize. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: C2 operand; coordinate names and argument positions have separate orders

Exact scalar-algebra check: unsupported.

partial-argument-symmetry

\frac{C2 operand; coordinate names and argument positions have separate orders; algorithm applicability checked}{Exchange mixed derivatives into ascending order} [partial-argument-symmetry]

Group: normalize. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: C2 operand; coordinate names and argument positions have separate orders

Exact scalar-algebra check: unsupported.

components-sum

\frac{Cartesian scalar entries}{(\begin{matrix} a \\ b \\ c \end{matrix}) + (\begin{matrix} d \\ e \\ f \end{matrix}) \to (\begin{matrix} a + d \\ b + e \\ c + f \end{matrix})} [components-sum]

Group: components. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Cartesian scalar entries

Exact scalar-algebra check: unsupported.

components-difference

\frac{Cartesian scalar entries}{(\begin{matrix} a \\ b \\ c \end{matrix}) - (\begin{matrix} d \\ e \\ f \end{matrix}) \to (\begin{matrix} a - d \\ b - e \\ c - f \end{matrix})} [components-difference]

Group: components. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Cartesian scalar entries

Exact scalar-algebra check: unsupported.

components-negation

\frac{Cartesian scalar entries}{- ((\begin{matrix} a \\ b \\ c \end{matrix})) \to (\begin{matrix} - a \\ - b \\ - c \end{matrix})} [components-negation]

Group: components. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Cartesian scalar entries

Exact scalar-algebra check: unsupported.

components-scale-left

\frac{s : scalar}{s \times (\begin{matrix} a \\ b \\ c \end{matrix}) \to (\begin{matrix} s \times a \\ s \times b \\ s \times c \end{matrix})} [components-scale-left]

Group: components. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Cartesian scalar entries

Exact scalar-algebra check: unsupported.

components-scale-right

\frac{s : scalar}{(\begin{matrix} a \\ b \\ c \end{matrix}) \times s \to (\begin{matrix} s \times a \\ s \times b \\ s \times c \end{matrix})} [components-scale-right]

Group: components. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Cartesian scalar entries

Exact scalar-algebra check: unsupported.

components-quotient

\frac{s : scalar}{\frac{(\begin{matrix} a \\ b \\ c \end{matrix})}{s} \to (\begin{matrix} \frac{a}{s} \\ \frac{b}{s} \\ \frac{c}{s} \end{matrix})} [components-quotient]

Group: components. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Cartesian scalar entries

Exact scalar-algebra check: unsupported.

components-dot

\frac{Cartesian scalar entries}{(\begin{matrix} a \\ b \\ c \end{matrix}) \cdot (\begin{matrix} d \\ e \\ f \end{matrix}) \to a \times d + b \times e + c \times f} [components-dot]

Group: components. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Cartesian scalar entries

Exact scalar-algebra check: unsupported.

components-cross

\frac{Cartesian scalar entries}{(\begin{matrix} a \\ b \\ c \end{matrix}) \times (\begin{matrix} d \\ e \\ f \end{matrix}) \to (\begin{matrix} b \times f - c \times e \\ c \times d - a \times f \\ a \times e - b \times d \end{matrix})} [components-cross]

Group: components. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Cartesian scalar entries

Exact scalar-algebra check: unsupported.

components-zero

\frac{Cartesian scalar entries}{\vec{0} \to (\begin{matrix} 0 \\ 0 \\ 0 \end{matrix})} [components-zero]

Group: components. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Cartesian scalar entries

Exact scalar-algebra check: unsupported.

gradient-components

\frac{differentiable (f) f : scalar; executable guards apply}{\nabla f \to (\begin{matrix} \frac{\partial}{\partial x} (f) \\ \frac{\partial}{\partial y} (f) \\ \frac{\partial}{\partial z} (f) \end{matrix})} [gradient-components]

Group: spatial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar field in an ordered Cartesian basis

Exact scalar-algebra check: unsupported.

Executable guards

((basiso facts x y z))

divergence-components

\frac{differentiable ((\begin{matrix} a \\ b \\ c \end{matrix})); executable guards apply}{\nabla \cdot ((\begin{matrix} a \\ b \\ c \end{matrix})) \to \frac{\partial}{\partial x} (a) + \frac{\partial}{\partial y} (b) + \frac{\partial}{\partial z} (c)} [divergence-components]

Group: spatial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 components in an ordered Cartesian basis

Exact scalar-algebra check: unsupported.

Executable guards

((basiso facts x y z))

curl-components

\frac{differentiable ((\begin{matrix} a \\ b \\ c \end{matrix})); executable guards apply}{\nabla \times ((\begin{matrix} a \\ b \\ c \end{matrix})) \to (\begin{matrix} \frac{\partial}{\partial y} (c) - \frac{\partial}{\partial z} (b) \\ \frac{\partial}{\partial z} (a) - \frac{\partial}{\partial x} (c) \\ \frac{\partial}{\partial x} (b) - \frac{\partial}{\partial y} (a) \end{matrix})} [curl-components]

Group: spatial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 components in an oriented ordered Cartesian basis

Exact scalar-algebra check: unsupported.

Executable guards

((basiso facts x y z))

laplacian-scalar-components

\frac{c2 (f) f : scalar}{Δ f \to \nabla \cdot (\nabla f)} [laplacian-scalar-components]

Group: spatial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C2 scalar field in Cartesian space

Exact scalar-algebra check: unsupported.

laplacian-vector-components

\frac{c2 ((\begin{matrix} a \\ b \\ c \end{matrix}))}{Δ ((\begin{matrix} a \\ b \\ c \end{matrix})) \to (\begin{matrix} Δ a \\ Δ b \\ Δ c \end{matrix})} [laplacian-vector-components]

Group: spatial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C2 Cartesian components

Exact scalar-algebra check: unsupported.

integrate-polynomial

\frac{Exact polynomials in independent coordinates and constant parameters; bounded sparse expansion; algorithm applicability checked}{The unique polynomial primitive with zero value at the integration coordinate's origin} [integrate-polynomial]

Group: polynomial-calculus. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: Exact polynomials in independent coordinates and constant parameters; bounded sparse expansion

Exact scalar-algebra check: unsupported.

solve-polynomial-poisson

\frac{Exact polynomials in independent coordinates and constant parameters; bounded sparse expansion; algorithm applicability checked}{A polynomial particular solution of Delta u = f, with zero initial value and first derivative in the selected axis} [solve-polynomial-poisson]

Exact scalar-algebra check: unsupported.

expand-polynomial

\frac{Exact polynomials in explicit coordinates/parameters; bounded expansion; algorithm applicability checked}{Exact sparse polynomial expansion} [expand-polynomial]

Group: polynomial-calculus. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: Exact polynomials in explicit coordinates/parameters; bounded expansion

Exact scalar-algebra check: unsupported.

math-rule->content把指定规则名转成文章内容：包括其结构化模式和可用说明。因此上面的规则卡片和运行时目录来自同一份定义，不会各自漂移。

若想只看写过说明的规则，可以约束documentation不等于#f：

((curl-curl-identity "Replace the curl of a curl by the gradient of the divergence minus the vector Laplacian. The field must be C2; declaring it divergence-free is a separate premise and a separate rewrite.") (grad-product "Differentiate the product of two scalar fields with the gradient product rule. C1 regularity suffices; no second derivatives or smoothness assumptions are required.") (curl-product "Expand the curl of a scalar times a vector field in oriented Cartesian space. The cross product is grad(f) cross E, in that order; reversing it changes the sign. Both factors need C1 regularity.") (differentiate-product "Generate the derivative of each factor separately and sum the two products. This rule constructs derivative terms; subsequent differentiation and simplification steps compute and reduce them.") (differentiate-quotient "Apply the quotient rule on the domain where the denominator is nonzero. The derivative remains a symbolic term until later passes process its operands and simplify the result.") (differentiate-function "Apply the shared function chain rule using one-based argument positions. C1 permits one derivative, C2 permits two, and smooth permits higher derivatives.") (cancel-common-factor "A check-only cancellation theorem. Its denominator side condition is explicit in the premise and must remain in the surrounding domain requirements.") (partial-function-chain "Apply the shared function chain rule using one-based argument positions. C1 permits one derivative, C2 permits two, and smooth permits higher derivatives."))

规则docstring解释其数学含义、适用条件或容易误解的细节，不会被当作新前提，也不会更改规则逻辑。这让说明可用于程序查询，同时保留普通Scheme函数的简单定义方式。

文章内容本身也是查询数据[#122]

规则目录不是唯一的数据源。Forester在分析阶段遍历每篇文章的内容IR，自动生成content-node relation。它记录节点所属页面、父节点、同级位置、类型、属性、纯文本投影和字符数；tag、taxon、link、subtree与math都是普通节点事实。

因为.plant在整个站点分析之前就已读取，跨文章查询应放在项目的#:analyze阶段。下面是Flora project.scm实际运行的查询：

(let ((nodes (content-node-relation forest)))
    (query (node-id page-id position text line column)
      (fresh (file)
        (math-containing-paragrapho nodes node-id)
        (shorter-than-o nodes node-id 120)
        (source-locationo nodes node-id file line column)
        (nodeo nodes
               (node-id node-id)
               (page-id page-id)
               (position position)
               (text text)))))

这会直接查询全站文章IR，不需要另外登记段落。查询结果由下面这个Flora项目本地的占位命令生成并放在此处：

匹配到 36 个短于 120 字且含公式的段落；下面展示前 6 个。

math-0006 (line 20, column 1; IR position 2): 输入是 ∇ × (−y, x, 0)；计算得到 0, 0, 2。
cfd-2-1 (line 51, column 3; IR position 7): 图2.1:有限控制体的定义(固定于空间中)。图例:流线;\Omega——控制体;\partial\Omega——控制体边界(封闭曲面);dS——面元;\vec{n}——外指单位法向量;\vec{v}——流动速度。
cfd-2-2-2 (line 253, column 5; IR position 17): 图2.2:作用在控制体表面元上的表面力。图例：\overline{\overline{\tau}}\cdot\vec{n}\,dS——黏性应力；p\vec{n}\,dS——压力；dS——面元；\Omega——控制体。
cfd-2-4-3 (line 671, column 5; IR position 4): 图2.4:薄边界层的表示。图例：Flow——流动；Boundary layer——边界层；Body contour——物面轮廓；\eta、\xi——贴体曲线坐标。
cfd-4-1-2 (line 185, column 5; IR position 2): 图4.2:三维中控制体一个面上法向量变化的情形。图例:阴影四边形为控制体的一个面;由于其四个顶点不共面ï¼面上的法向量(图中\vec{n}_1、\vec{n}_2)随位置变化ï¼不再是常向量。
cfd-4-3-3 (line 1361, column 22; IR position 0): |\bar{A}_{Roe}|与左、右状态之差的乘积可以高效地计算如下en

同一份节点关系也能查普通文本和metadata。plain-text-paragrapho选择只有文本子节点的段落；contains-texto检查文本投影中是否包含指定字符串；topic-membero通过相同的关系查询tag和taxon。例如把topic ID固定为tutorial，会返回所有相应页面。

node-id只在本次分析结果中有效，不应保存成外部引用。source-locationo会返回节点对应的源文件、行和列；Flora的结果列表会同时展示源码行列号与IR同级位置。若一个段落由多行文本和内联命令组成，段落位置取其第一个有位置的子节点，内联命令则保留自己的起始位置。若需要定位到IR中更具体的节点，可以沿parent-id与position回溯。公式的纯文本投影会保留幂、下标和分数的可读边界，例如x^(2)与(a)/(b)，避免把结构挤成难读的x2或ab。

查询结果也是教程内容[#123]

上面的模式串、行数、规则卡片和文章内容查询结果都在构建时现场计算。若文章或规则变化，查询结果会随之更新。它展示了Grove的通用写作方式：保留Scheme值与内容树，让renderer负责最终HTML。

从首页回顾全站路线，或打开数学表示层继续实验。