Documentation

Lean.Elab.PreDefinition.WF.PackMutual

Equations
Instances For

    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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For