mathlib documentation

tactic.omega.term

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  :
()omega.term

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