Documentation

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.