{motive : Lean.PrettyPrinter.Delaborator.AppMatchState → Sort u} →
  ((info : Lean.Meta.MatcherInfo) →
      (matcherTy : Lean.SubExpr) →
        (motive_1 : Option (Lean.Term × Lean.Expr)) →
          (motiveNamed : Bool) →
            (discrs : Array Lean.Term) →
              (hNames? : Array (Option Lean.Name)) →
                (alts : Array Lean.SubExpr) →
                  (varNames : Array (Array Lean.Name)) →
                    (rhss : Array Lean.Term) →
                      motive
                        { info := info, matcherTy := matcherTy, motive := motive_1, motiveNamed := motiveNamed,
                          discrs := discrs, hNames? := hNames?, alts := alts, varNames := varNames, rhss := rhss }) →
    (t : Lean.PrettyPrinter.Delaborator.AppMatchState) → motive t