Zulip Chat Archive

Stream: general

Topic: Suggest tactic missing a suggestion


Michael Stoll (Jan 24 2023 at 21:31):

Consider this:

import algebra.group.basic
import data.real.basic
import tactic.suggest

-- this produces only a list of unhelpful too general things:
-- Try this: refine eq.symm _
-- Try this: refine eq_comm.mp _
-- Try this: refine eq_comm.mpr _
-- Try this: refine inv_inj.mp _  etc.
example (a b : ) : a + (b - a) = b := by suggest

-- However, we have
example (a b : ) : a + (b - a) = b := add_sub_cancel'_right a b

Why does suggestnot find the exact match?


Last updated: Dec 20 2023 at 11:08 UTC