mathlib documentation

tactic.omega.term

@[protected, instance]
def omega.term  :
Type

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

Equations
@[simp]
def omega.term.val (v : ) :

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_mul {v : } {i : } {t : omega.term} :
theorem omega.term.val_div {v : } {i b : } {as : list } :
i b(∀ (x : ), x asi 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