Lean4
/-- Return the link text and inserted text above and below of the conv widget. -/
@[nolint unusedArguments]
def insertEnter (locations : Array Lean.SubExpr.GoalsLocation) (goalType : Expr) (params : SelectInsertParams) :
MetaM (String × String × Option (String.Pos × String.Pos)) := do
let some pos := locations[0]? |
throwError"You must select something."
let (fvar, subexprPos) ←
match pos with
| ⟨_, .target subexprPos⟩ =>
pure (none, subexprPos)
| ⟨_, .hypType fvar subexprPos⟩ =>
pure (some fvar, subexprPos)
| ⟨_, .hypValue fvar subexprPos⟩ =>
pure (some fvar, subexprPos)
| _ =>
throwError"You must select something in the goal or in a local value."
let mut list := (SubExpr.Pos.toArray subexprPos).toList
let mut expr := goalType
let mut retList :=
[]
-- generate list of commands for `enter`
while !list.isEmpty do
let res ← solveLevel expr list
expr := res.expr
retList :=
match res.val? with
| none => retList
| some val => val :: retList
list := res.listRest
retList := List.reverse retList
let spc := String.replicate (SelectInsertParamsClass.replaceRange params).start.character ' '
let loc ←
match fvar with
| some fvarId =>
pure s!"at {← fvarId.getUserName} "
| none =>
pure ""
let mut enterval := s! "conv {loc }=>\n{spc } enter {retList}"
if enterval.contains '0' then
enterval := "Error: Not a valid conv target"
if retList.isEmpty then
enterval := ""
return ("Generate conv", enterval, none)
