mathlib documentation

tactic.omega.int.main

Given a (p : preform), return the expr of a (t : univ_close m p)

Reification to imtermediate shadow syntax that retains exprs

Reification to imtermediate shadow syntax that retains exprs

List of all unreified exprs

List of all unreified exprs

Reification to an intermediate shadow syntax which eliminates exprs, but still includes non-canonical terms

Reification to an intermediate shadow syntax which eliminates exprs, but still includes non-canonical terms

Reification to an intermediate shadow syntax which eliminates exprs, but still includes non-canonical terms.

meta def omega.int.prove  :

Return expr of proof of current LIA goal

meta def omega.int.eq_int (x : expr) :

Succeed iff argument is the expr of ℤ

meta def omega.int.wff  :

Check whether argument is expr of a well-formed formula of LIA

meta def omega.int.wfx (x : expr) :

Succeed iff argument is expr of term whose type is wff

Intro all universal quantifiers over ℤ

If the goal has universal quantifiers over integers, introduce all of them. Otherwise, revert all hypotheses that are formulas of linear integer arithmetic.

meta def omega_int (is_manual : bool) :

The core omega tactic for integers.