Commit 2026-01-13 15:36 55c8e3f0

fix(Tactic/Widget/Conv): fix various issues (#25889) Fixes various issues with the conv? widget. Closes #25162. This is essentially a complete rewrite of the conv? widget. (Zulip thread) Specifically, fixes issues with conv? where

• when converting a SubExpr.Pos to conv directions, it always uses the goal expression as reference, even when working on a hypothesis, this often leads to bad results and makes it unusable on hypotheses
• it refuses to go all the way in to a function (for example in Nat.succ 0, you can't access Nat.succ)
• it refuses to enter binders where the name of the bound variable contains the character 0 (try it on ∀ (x0 : Nat), x0 = x0)
• it panics if it can't find a binder name instead of just coming up with one itself, this also means usually you can't enter either side of a non-dependent arrow since those usually don't have binder names (try it on False → False)
• you can't enter the type of a binder, you end up going into the body instead (try it on fun (x : False) => (x.elim : False → Nat) x.elim)
• you can't partially enter a function, you end up going to the top argument after instead (for example, in the expression id (id id) 0, when you click on id (id id), you end up going to id id)