pub fn parse_lin(t: &ProofTerm) -> Option<LinExpr>Expand description
Parse a ProofTerm into a linear expression, or None if it is non-linear
(e.g. mul of two non-constants). Numeric constants are literals; other names
are variables; add/sub/mul build the form.