mathlib3 documentation

tactic.omega.term

@[protected, instance]
def omega.term  :

Shadow syntax of normalized terms. The first element represents the constant term and the list represents the coefficients.

Equations
Instances for omega.term
@[protected, instance]
@[simp]

Evaluate a term using the valuation v.

Equations
@[simp]
Equations
@[simp]
Equations
@[simp]
Equations
@[simp]
Equations
@[simp]
Equations
@[simp]
theorem omega.term.val_sub {v : } {t1 t2 : omega.term} :
@[simp]
theorem omega.term.val_add {v : } {t1 t2 : omega.term} :
@[simp]
theorem omega.term.val_div {v : } {i b : } {as : list } :
i b ( (x : ), x as i x) omega.term.val v (omega.term.div i (b, as)) = omega.term.val v (b, as) / i

Fresh de Brujin index not used by any variable ocurring in the term

Equations
Equations

Fresh de Brujin index not used by any variable ocurring in the list of terms

Equations