mathlib documentation

Return expr of proof that argument is free of subtractions

Return expr of proof that argument is free of negations

Return expr of proof that argument is free of subtractions

Given a p : preform, return the expr of a term t : p.unsat, where p is subtraction- and negation-free.

Given a p : preform, return the expr of a term t : p.unsat, where p is negation-free.

Given a (m : nat) and (p : preform), return the expr of (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 LNA goal

Succeed iff argument is expr of ℕ

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

Succeed iff argument is expr of term whose type is wff

Intro all universal quantifiers over nat

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

The core omega tactic for natural numbers.