# mathlibdocumentation

tactic.omega.int.preterm

meta inductive omega.int.exprterm  :
Type
• cst :
• exp :

The shadow syntax for arithmetic terms. All constants are reified to cst (e.g., -5 is reified to cst -5) and all other atomic terms are reified to exp (e.g., -5 * (gcd 14 -7) is reified to exp -5 \(gcd 14 -7)). expaccepts a coefficient of typeint as its first argument because multiplication by constant is allowed by the omega test.

@[instance]

@[instance]

inductive omega.int.preterm  :
Type
• cst :
• var :

Similar to exprterm, except that all exprs are now replaced with de Brujin indices of type nat`. This is akin to generalizing over the terms represented by the said exprs.

@[simp]
def omega.int.preterm.val  :
()

Preterm evaluation

Equations

Fresh de Brujin index not used by any variable in argument

Equations
@[simp]

Equations

Equations
@[simp]

Return a term (which is in canonical form by definition) that is equivalent to the input preterm

Equations
@[simp]
theorem omega.int.val_canonize {v : } {t : omega.int.preterm} :