simp? tactic

Stream: general

[Frederick Pu]

How does the simp tactic create an edit link to produce simp only [blah blahb blah]? Can I replicate this behavior using proof widgets and MakeEditLink?

[Alex J. Best]

You can use https://leanprover-community.github.io/mathlib4_docs/Std/Tactic/TryThis.html#Std.Tactic.TryThis.addSuggestion for this, which uses proofwidgets. What is makeeditlink?

[Frederick Pu]

make edit link is a thing from the ProofWidget library. I'm trying to make a widget that allows the user to draw a contour on the cartesion plane which then gets automatically turned into a let definition

[Patrick Massot]

You can take inspiration from widget code at https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Widget/SelectPanelUtils.lean or https://github.com/PatrickMassot/verbose-lean4/blob/master/Verbose/Tactics/Widget.lean