mathlib documentation

tactic.omega.main

source
meta def omega.select_domain (t s : tactic (option bool)) :
tactic (option bool)
source
meta def omega.type_domain (x : expr) :
tactic (option bool)
source
meta def omega.form_domain  :
expr → tactic (option bool)

Detects domain of a formula from its expr.

  • Returns none, if domain can be either ℤ or ℕ
  • Returns some tt, if domain is exclusively ℤ
  • Returns some ff, if domain is exclusively ℕ
  • Fails, if domain is neither ℤ nor ℕ
source
meta def omega.goal_domain_aux (x : expr) :
tactic bool
source
meta def omega.goal_domain  :
tactic bool

Use the current goal to determine. Return tt if the domain is ℤ, and return ff if it is ℕ

source
meta def omega.determine_domain (opt : list name) :
tactic bool

Return tt if the domain is ℤ, and return ff if it is ℕ

source
meta def tactic.interactive.omega (opt : interactive.parse lean.parser.ident*) :
tactic unit

Attempts to discharge goals in the quantifier-free fragment of linear integer and natural number arithmetic using the Omega test. Guesses the correct domain by looking at the goal and hypotheses, and then reverts all relevant hypotheses and variables. Use omega manual to disable automatic reverts, and omega int or omega nat to specify the domain.