pub fn identity(
lhs: &TensorGraph,
rhs: &TensorGraph,
) -> Result<Obligation, SmtError>Expand description
The obligation that two programs compute every tensor both keep alike when their products, elementwise sums and
products and scales are computed exactly — an algebraic identity at the shapes the programs declare. Every other op
is left open as obligation leaves it.