mathlib documentation

tactic.omega.int.form

inductive omega.int.preform  :
Type

Intermediate shadow syntax for LIA formulas that includes non-canonical terms

@[simp]
def omega.int.univ_close  :
omega.int.preform() → Prop

univ_close p n := p closed by prepending n universal quantifiers

Equations

All valuations satisfy argument

Equations

There exists some valuation that satisfies argument

Equations

implies p q := under any valuation, q holds if p holds

Equations

equiv p q := under any valuation, p holds iff q holds

Equations

There does not exist any valuation that satisfies argument

Equations

Equations

Tactic for setting up proof by induction over preforms.