mathlib documentation

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.

Return expr of proof of current LIA goal

Succeed iff argument is the expr of ℤ

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

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.

The core omega tactic for integers.