{motive : Lean.Elab.Command.Context → Sort u} →
  (t : Lean.Elab.Command.Context) →
    ((fileName : String) →
        (fileMap : Lean.FileMap) →
          (currRecDepth : ℕ) →
            (cmdPos : String.Pos.Raw) →
              (macroStack : Lean.Elab.MacroStack) →
                (quotContext? : Option Lean.Name) →
                  (currMacroScope : Lean.MacroScope) →
                    (ref : Lean.Syntax) →
                      (snap? : Option (Lean.Language.SnapshotBundle Lean.Language.DynamicSnapshot)) →
                        (cancelTk? : Option IO.CancelToken) →
                          (suppressElabErrors : Bool) →
                            motive
                              { fileName := fileName, fileMap := fileMap, currRecDepth := currRecDepth,
                                cmdPos := cmdPos, macroStack := macroStack, quotContext? := quotContext?,
                                currMacroScope := currMacroScope, ref := ref, snap? := snap?, cancelTk? := cancelTk?,
                                suppressElabErrors := suppressElabErrors }) →
      motive t