-- Lean.Elab.PreDefinition.TerminationMeasure
_private.Lean.Elab.PreDefinition.TerminationMeasure.0.Lean.Elab.TerminationMeasure.delab.go.eq_def : ∀ (measure : Lean.Elab.TerminationMeasure) (a : ℕ) (a_1 : Lean.TSyntaxArray `ident),
  Lean.Elab.TerminationMeasure.delab.go✝ measure a a_1 =
    match a, a_1 with
    | 0, vars => do
      let stxBody ← Lean.PrettyPrinter.Delaborator.delab
      let hole ←
        do
          let info ← Lean.MonadRef.mkInfoFromRefPos
          let _ ← Lean.getCurrMacroScope
          let _ ← Lean.MonadQuotation.getContext
          pure { raw := Lean.Syntax.node1 info `Lean.Parser.Term.hole (Lean.Syntax.atom info "_") }
      have vars : Lean.TSyntaxArray [`ident, `Lean.Parser.Term.hole] :=
        Array.map
          (fun i =>
            if Lean.Syntax.hasIdent (Lean.TSyntax.getId i) stxBody.raw = true then { raw := i.raw }
            else { raw := hole.raw })
          vars
      have vars : Lean.TSyntaxArray [`ident, `Lean.Parser.Term.hole] := vars
      let __s ←
        forIn { } vars fun x __s =>
            have vars := __s;
            if (!Array.isEmpty vars && (Array.back! vars).raw.isOfKind `Lean.Parser.Term.hole) = true then
              have vars := Array.pop vars;
              pure (ForInStep.yield vars)
            else pure (ForInStep.done vars)
      have vars : Lean.TSyntaxArray [`ident, `Lean.Parser.Term.hole] := __s
      if measure.structural = true then
          if Array.isEmpty vars = true then do
            let info ← Lean.MonadRef.mkInfoFromRefPos
            let _ ← Lean.getCurrMacroScope
            let _ ← Lean.MonadQuotation.getContext
            pure
                {
                  raw :=
                    Lean.Syntax.node4 info `Lean.Parser.Termination.terminationBy
                      (Lean.Syntax.atom info "termination_by")
                      (Lean.Syntax.node1 info `null (Lean.Syntax.atom info "structural"))
                      (Lean.Syntax.node info `null #[]) stxBody.raw }
          else do
            let info ← Lean.MonadRef.mkInfoFromRefPos
            let _ ← Lean.getCurrMacroScope
            let _ ← Lean.MonadQuotation.getContext
            pure
                {
                  raw :=
                    Lean.Syntax.node4 info `Lean.Parser.Termination.terminationBy
                      (Lean.Syntax.atom info "termination_by")
                      (Lean.Syntax.node1 info `null (Lean.Syntax.atom info "structural"))
                      (Lean.Syntax.node2 info `null (Lean.Syntax.node info `null (#[].append vars.raw))
                        (Lean.Syntax.atom info "=>"))
                      stxBody.raw }
        else
          if Array.isEmpty vars = true then do
            let info ← Lean.MonadRef.mkInfoFromRefPos
            let _ ← Lean.getCurrMacroScope
            let _ ← Lean.MonadQuotation.getContext
            pure
                {
                  raw :=
                    Lean.Syntax.node4 info `Lean.Parser.Termination.terminationBy
                      (Lean.Syntax.atom info "termination_by") (Lean.Syntax.node info `null #[])
                      (Lean.Syntax.node info `null #[]) stxBody.raw }
          else do
            let info ← Lean.MonadRef.mkInfoFromRefPos
            let _ ← Lean.getCurrMacroScope
            let _ ← Lean.MonadQuotation.getContext
            pure
                {
                  raw :=
                    Lean.Syntax.node4 info `Lean.Parser.Termination.terminationBy
                      (Lean.Syntax.atom info "termination_by") (Lean.Syntax.node info `null #[])
                      (Lean.Syntax.node2 info `null (Lean.Syntax.node info `null (#[].append vars.raw))
                        (Lean.Syntax.atom info "=>"))
                      stxBody.raw }
    | i.succ, vars => do
      let e ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr
      if e.isLambda = true then
          Lean.PrettyPrinter.Delaborator.withBindingBodyUnusedName fun n =>
            Lean.Elab.TerminationMeasure.delab.go✝ measure i (Array.push vars { raw := n })
        else Lean.Elab.TerminationMeasure.delab.go✝ measure 0 vars