waynee95 (Mar 28 2023 at 08:47): waynee95 (Mar 28 2023 at 08:47):Quite often I would like to have sledgehammer find a proof using an explicit fact by name and not just based on simp. How could I restrict sledgehammer to not find a proof by simp or auto?
Gergely Buday (Mar 28 2023 at 10:16):sledgehammer [dont_try0]
This only uses metis and not the automatic tools
Wolfgang Jeltsch (Mar 28 2023 at 14:26):Since when does Sledgehammer try the basic tools? What I know is that Sledgehammer precisely doesn’t use those tools that try0 tries, and part of the point of try is to employ both try0 and sledgehammer.
Mathias Fleury (Mar 28 2023 at 16:41):no no no no
Mathias Fleury (Mar 28 2023 at 16:41):we had this discussion on the mailing list recently
Mathias Fleury (Mar 28 2023 at 16:42):sledgehammer has an option that only tries metis to reconstruct proof steps (no auto, so simp, no blast, ...)
Mathias Fleury (Mar 28 2023 at 16:42):this option is called dont_try0
Mathias Fleury (Mar 28 2023 at 16:42):It has absolutely nothing to do with the try0 command
Kevin Kappelmann (Mar 29 2023 at 05:45):Last updated: Nov 13 2025 at 08:29 UTC