∀ (views : Array Lean.Elab.Command.InductiveView) (i : ℕ) (acc : Array Lean.Elab.Command.PreElabHeaderResult),
  Lean.Elab.Command.elabHeadersAux✝ views i acc =
    Lean.Elab.Term.withAutoBoundImplicitForbiddenPred (fun n => views.any fun x => x.shortDeclName == n)
      (if h : i < views.size then
        have view := views[i];
        do
        let acc ←
          Lean.withRef view.ref
              (Lean.Elab.Term.withAutoBoundImplicit
                (Lean.Elab.Term.elabBinders view.binders.getArgs fun params => do
                  let __discr ←
                    Lean.Elab.Term.withAutoBoundImplicit do
                        let typeStx ←
                          view.type?.getDM do
                              let info ← Lean.MonadRef.mkInfoFromRefPos
                              let _ ← Lean.getCurrMacroScope
                              let _ ← Lean.MonadQuotation.getContext
                              pure
                                  {
                                      raw :=
                                        Lean.Syntax.node2 info `Lean.Parser.Term.sort (Lean.Syntax.atom info "Sort")
                                          (Lean.Syntax.node1 info `null
                                            (Lean.Syntax.node1 info `Lean.Parser.Level.hole
                                              (Lean.Syntax.atom info "_"))) }.raw
                        let type ← Lean.Elab.Term.elabType typeStx
                        Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing
                        have inlayHintPos? : Option String.Pos.Raw :=
                          view.binders.getTailPos? true <|> view.declId.getTailPos? true
                        let indices ← Lean.Elab.Term.addAutoBoundImplicits #[] inlayHintPos?
                        let type ← liftM (Lean.Meta.mkForallFVars indices type)
                        have __do_jp : PUnit.{1} → Lean.Elab.TermElabM (Lean.Expr × ℕ) := fun y =>
                          pure (type, indices.size)
                        if view.allowIndices = true then do
                            let __do_lift ← liftM (Lean.Meta.isTypeFormerType type)
                            if __do_lift = true then do
                                let y ← pure PUnit.unit
                                __do_jp y
                              else do
                                let y ←
                                  Lean.throwErrorAt typeStx
                                      (Lean.toMessageData
                                          "Invalid resulting type: Expected a sort or an indexed family of sorts" ++
                                        (Lean.toMessageData
                                            "Examples of valid sorts include `Type _`, `Sort _`, and `Prop`").hint')
                                __do_jp y
                          else do
                            let __do_lift ← liftM (Lean.Meta.whnfD type)
                            if __do_lift.isSort = true then do
                                let y ← pure PUnit.unit
                                __do_jp y
                              else do
                                let y ←
                                  Lean.throwErrorAt typeStx
                                      (Lean.toMessageData "Invalid resulting type: Expected a sort" ++
                                        (Lean.toMessageData
                                            "Examples of valid sorts include `Type _`, `Sort _`, and `Prop`").hint')
                                __do_jp y
                  match __discr with
                    | (type, snd) => do
                      let params ← Lean.Elab.Term.addAutoBoundImplicits params (view.declId.getTailPos? true)
                      have cls : Lean.Name := `Elab.inductive
                      let __do_lift ← Lean.isTracingEnabledFor cls
                      have __do_jp : Unit → Lean.Elab.TermElabM (Array Lean.Elab.Command.PreElabHeaderResult) :=
                        fun y => do
                        let levelNames ← Lean.Elab.Term.getLevelNames
                        let type ← liftM (Lean.Meta.mkForallFVars params type)
                        pure
                            (acc.push
                              { view := view, levelNames := levelNames, numParams := params.size, type := type,
                                origParams := params })
                      if __do_lift = true then do
                          let y ←
                            Lean.addTrace cls
                                (Lean.toMessageData "header params: " ++ Lean.toMessageData params ++
                                    Lean.toMessageData ", type: " ++
                                  Lean.toMessageData type)
                          __do_jp y
                        else do
                          let y ← pure PUnit.unit
                          __do_jp y))
        Lean.Elab.Command.elabHeadersAux✝¹ views (i + 1) acc
      else pure acc)