mathlib3 documentation

tactic.omega.int.main

source
meta def simp_attr.sugar  :
(user_attribute simp_lemmas)
source
meta def omega.int.desugar  :
tactic unit
source
theorem omega.int.univ_close_of_unsat_clausify (m : ℕ) (p : omega.int.preform) :
omega.clauses.unsat (omega.int.dnf p.not) → omega.int.univ_close p (λ (x : ℕ), 0) m
source
meta def omega.int.prove_univ_close (m : ℕ) (p : omega.int.preform) :
tactic expr

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

source
meta def omega.int.to_exprterm  :
expr → tactic omega.int.exprterm

Reification to imtermediate shadow syntax that retains exprs

source
meta def omega.int.to_exprform  :
expr → tactic omega.int.exprform

Reification to imtermediate shadow syntax that retains exprs

source
meta def omega.int.exprterm.exprs  :
omega.int.exprterm → list expr

List of all unreified exprs

source
meta def omega.int.exprform.exprs  :
omega.int.exprform → list expr

List of all unreified exprs

source
meta def omega.int.exprterm.to_preterm (xs : list expr) :
omega.int.exprterm → tactic omega.int.preterm

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

source
meta def omega.int.exprform.to_preform (xs : list expr) :
omega.int.exprform → tactic omega.int.preform

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

source
meta def omega.int.to_preform (x : expr) :
tactic (omega.int.preform × ℕ)

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

source
meta def omega.int.prove  :
tactic expr

Return expr of proof of current LIA goal

source
meta def omega.int.eq_int (x : expr) :
tactic unit

Succeed iff argument is the expr of ℤ

source
meta def omega.int.wff  :
expr → tactic unit

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

source
meta def omega.int.wfx (x : expr) :
tactic unit

Succeed iff argument is expr of term whose type is wff

source
meta def omega.int.intro_ints_core  :
tactic unit

Intro all universal quantifiers over ℤ

source
meta def omega.int.intro_ints  :
tactic unit
source
meta def omega.int.preprocess  :
tactic unit

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

source
meta def omega_int (is_manual : bool) :
tactic unit

The core omega tactic for integers.