# Documentation

Init.Data.Nat.Linear

Helper definitions and theorems for constructing linear arithmetic proofs.

@[inline]
Equations
@[inline]
Equations

When encoding polynomials. We use fixedVar for encoding numerals. The denotation of fixedVar is always 1.

Equations
Equations
• = bif then 1 else
• num:
• var:
• mulL:
• mulR:
Instances For
@[inline]
Equations
Equations
Equations
Equations
Equations
Equations
• = bif k == 0 then [] else bif k == 1 then p else
Equations
Equations
Equations
Equations
Equations
• = match p with | [] => some 0 | [(k, v)] => bif then some k else none | x => none
Equations
• = match p with | [] => true | x => false
Equations
Equations
• One or more equations did not get rendered due to their size.
• = p₁ ++ p₂
Equations
• = bif k == 0 then [] else []
• = [(1, i)]
Equations
Equations
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• = bif c.eq then && else
Equations
• = { eq := c.eq, lhs := , rhs := }
Equations
• One or more equations did not get rendered due to their size.
@[inline]
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• = bif then else bif k == 1 then else
Equations
• = match p with | [] => | (k, v) :: p =>
Equations
Equations
• = { eq := c.eq, lhs := , rhs := }