Lean4
/-- Return the link text and inserted text above and below of the congrm widget. -/
@[nolint unusedArguments]
def makeCongrMString (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Expr) (_ : SelectInsertParams) :
MetaM (String × String × Option (String.Pos × String.Pos)) := do
let subexprPos := getGoalLocations pos
unless goalType.isAppOf ``Eq || goalType.isAppOf ``Iff do
throwError"The goal must be an equality or iff."
let mut goalTypeWithMetaVars := goalType
for pos in subexprPos do
goalTypeWithMetaVars ← insertMetaVar goalTypeWithMetaVars pos
let side := if subexprPos[0]!.toArray[0]! = 0 then 1 else 2
let sideExpr := goalTypeWithMetaVars.getAppArgs[side]!
let res := "congrm " ++ (toString (← Meta.ppExpr sideExpr)).renameMetaVar
return (res, res, none)
