def Lean.Elab.WF.withFixedPrefix {α : Type} (fixedPrefix : Nat) (preDefs : Array Lean.Elab.PreDefinition) (k : Array Lean.Expr → Array Lean.Expr → Array Lean.Expr → Lean.MetaM α) : Lean.MetaM α

partial def Lean.Elab.WF.withFixedPrefix.go {α : Type} (preDefs : Array Lean.Elab.PreDefinition) (k : Array Lean.Expr → Array Lean.Expr → Array Lean.Expr → Lean.MetaM α) (i : Nat) (fvars : Array Lean.Expr) (vals : Array Lean.Expr) : Lean.MetaM α

def Lean.Elab.WF.packMutual (fixedPrefix : Nat) (preDefsOriginal : Array Lean.Elab.PreDefinition) (preDefs : Array Lean.Elab.PreDefinition) : Lean.MetaM Lean.Elab.PreDefinition

If preDefs.size > 1, combine different functions in a single one using PSum. This method assumes all preDefs have arity 1, and have already been processed using packDomain. Here is a small example. Suppose the input is

f x :=
  match x.2.1, x.2.2.1, x.2.2.2 with
  | 0, a, b => a
  | Nat.succ n, a, b => (g ⟨x.1, n, a, b⟩).fst
g x :=
  match x.2.1, x.2.2.1, x.2.2.2 with
  | 0, a, b => (a, b)
  | Nat.succ n, a, b => (h ⟨x.1, n, a, b⟩, a)
h x =>
  match x.2.1, x.2.2.1, x.2.2.2 with
  | 0, a, b => b
  | Nat.succ n, a, b => f ⟨x.1, n, a, b⟩

this method produces the following pre definition

f._mutual x :=
  PSum.casesOn x
    (fun val =>
      match val.2.1, val.2.2.1, val.2.2.2 with
      | 0, a, b => a
      | Nat.succ n, a, b => (f._mutual (PSum.inr (PSum.inl ⟨val.1, n, a, b⟩))).fst
    fun val =>
      PSum.casesOn val
        (fun val =>
          match val.2.1, val.2.2.1, val.2.2.2 with
          | 0, a, b => (a, b)
          | Nat.succ n, a, b => (f._mutual (PSum.inr (PSum.inr ⟨val.1, n, a, b⟩)), a)
        fun val =>
          match val.2.1, val.2.2.1, val.2.2.2 with
          | 0, a, b => b
          | Nat.succ n, a, b =>
            f._mutual (PSum.inl ⟨val.1, n, a, b⟩)

Remark: preDefsOriginal is used for error reporting, it contains the definitions before applying packDomain.