_aux_Mathlib_Tactic_CongrM___elabRules_Mathlib_Tactic_congrM_1

Lean4
@[tactic Mathlib.Tactic.congrM]
public meta def _aux_Mathlib_Tactic_CongrM___elabRules_Mathlib_Tactic_congrM_1 : Lean.Elab.Tactic.Tactic✝ := fun
  | `(tactic| congrm $expr:term) => do
    -- Wrap all synthetic holes `?m` as `c(?m)` to form `congr(...)` pattern

    let pattern ←
      expr.raw.replaceM fun stx =>
          if stx.isOfKind ``Parser.Term.syntheticHole then pure <| stx.mkAntiquotNode `term
          else
            if stx.isAntiquots then
                -- Don't look into `$(..)` expressions
                 pure stx
            else pure none
    trace[Tactic.congrm]"pattern: {pattern}"
    liftMetaTactic fun g => do
        return
          [← (← g.iffOfEq).liftReflToEq]
            -- Apply `congr(...)`

    withMainContext do
        let gStx ←
          Term.exprToSyntax
              (← getMainTarget)
                -- Gives the expected type to `refine` as a workaround for its elaboration order.

        evalTactic <| ← `(tactic| refine without_cdot(congr($(⟨pattern⟩)) : $gStx))
  | _ => no_error_if_unused% throwUnsupportedSyntax✝
Похожие утверждения