# mathlibdocumentation

tactic.omega.nat.main

meta def omega.nat.desugar  :
theorem omega.nat.univ_close_of_unsat_neg_elim_not (m : ) (p : omega.nat.preform) :
(λ (_x : ), 0) m

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

meta def omega.nat.to_preform (x : expr) :

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

meta def omega.nat.prove  :

Return expr of proof of current LNA goal

meta def omega.nat.eq_nat (x : expr) :

Succeed iff argument is expr of ℕ

meta def omega.nat.wff  :

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

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

Succeed iff argument is expr of term whose type is wff

Intro all universal quantifiers over nat

meta def omega.nat.preprocess  :

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

meta def omega_nat (is_manual : bool) :

The core omega tactic for natural numbers.