Zulip Chat Archive

Stream: general

Topic: The omega tactic


view this post on Zulip Donald Sebastian Leung (Mar 01 2020 at 06:14):

The omega tactic is currently documented in the Lean mathlib documentation but this simple example fails with unknown identifier 'omega':

example : 1 + 1 = 2 :=
begin
  omega
end

How do I import the omega tactic?

view this post on Zulip Alex J. Best (Mar 01 2020 at 06:15):

import tactic.omega

view this post on Zulip Donald Sebastian Leung (Mar 01 2020 at 06:16):

Thanks, that worked

view this post on Zulip Floris van Doorn (Mar 02 2020 at 20:46):

In general, if you write import tactic you get all tactics in mathlib.


Last updated: May 08 2021 at 04:14 UTC