Conv widget

This is a slightly improved version of one of the examples that used to be in the ProofWidgets library. It defines a conv? tactic that displays a widget panel allowing to generate a conv call zooming to the subexpression selected in the goal.

inductive Mathlib.Tactic.Conv.Path : Type

A path to a subexpression from a root expression. The constructors are chosen to be easily translatable into conv directions.

• arg (arg : ℕ) (all : Bool) (next : Path) : Path

  Accesses the argth implicit or explicit argument, depending on whether all is true or false, respectively. Corresponds to the conv tactic arg. For example, Path.arg 3 true next is arg @3 followed by next, and Path.arg 0 false next is arg 0 followed by next.

• fun (depth : ℕ) : Path

  End a conv sequence with depth-many repetitions of the conv tactic fun. For example, Path.fun 3 corresponds to the conv sequence fun; fun; fun, and Path.fun 0 just terminates a Path without any extra conv tactics.

• type (next : Path) : Path

  Traverses into the binder type of a forall, let, or lambda. Currently out of these three options conv only supports going into the binder type of a forall, but in the future if conv gets support for going into let or lambda binding types with different conv tactics we may add additional arguments to specify whether the binder is a forall, let, or lambda. Corresponds to the conv tactics lhs or arg.

• body (name : Lean.Name) (next : Path) : Path

  Traverses into the body of a forall, let, or lambda. Corresponds to the conv tactics intro or ext.

def Mathlib.Tactic.Conv.Path.ofSubExprPos (expr : Lean.Expr) (pos : Lean.SubExpr.Pos) : Lean.MetaM Path

Given an e : Expr and pos : SubExpr.Pos, Path.ofSubExprPos expr pos generates the Path corresponding to traversing pos starting at the reference expression e.

def Mathlib.Tactic.Conv.pathToStx {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (convStx : Lean.TSyntax `conv) (path : Path) (loc : Option Lean.Name) (xs : Lean.Syntax.TSepArray `Lean.Parser.Tactic.Conv.enterArg "," := ∅) : m (Lean.TSyntax `tactic)

Given a path : Path and xs : TSepArray ``enterArg ",", generate the conv syntax corresponding to enter [xs,*] followed by traversing path. If loc is some fvar, start with conv at fvar =>, otherwise if loc is none start with conv =>.

def Mathlib.Tactic.Conv.insertEnterSyntax (locations : Array Lean.SubExpr.GoalsLocation) (goalType : Lean.Expr) : Lean.MetaM Lean.Syntax

Return the syntax to insert for the conv widget. Factored out of insertEnter for easy testing.

def Mathlib.Tactic.Conv.insertEnter (locations : Array Lean.SubExpr.GoalsLocation) (goalType : Lean.Expr) (params : SelectInsertParams) : Lean.MetaM (String × String × Option (String.Pos.Raw × String.Pos.Raw))

Return the text for the link in the conv widget that inserts the replacement, and also return the replacement, and the range within the file to highlight after the replacement is inserted. The highlighted range will always be the trailing skip.

def Mathlib.Tactic.Conv.SelectionPanel.rpc (params : SelectInsertParams) : Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)

Rpc function for the conv widget.

def Mathlib.Tactic.Conv.SelectionPanel : ProofWidgets.Component SelectInsertParams

The conv widget.

def Mathlib.Tactic.Conv.tacticConv? : Lean.ParserDescr

Display a widget panel allowing to generate a conv call zooming to the subexpression selected in the goal or in the type of a local hypothesis or let-decl.