def Lean.Elab.WF.withAppN (n : Nat) (e : Lean.Expr) (k : Array Lean.Expr → Lean.MetaM Lean.Expr) : Lean.MetaM Lean.Expr

Pass the first n arguments of e to the continuation, and apply the result to the remaining arguments. If e does not have enough arguments, it is eta-expanded as needed.

Unlike Meta.etaExpand does not use withDefault.

Equations

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

def Lean.Elab.WF.mkMutualArg (numFuncs : Nat) (domain : Lean.Expr) (fidx : Nat) (arg : Lean.Expr) : Lean.MetaM Lean.Expr

If arg is the argument to the fidxth of the numFuncs in the recursive group, then mkMutualArg packs that argument in PSum.inl and PSum.inr constructors to create the mutual-packed argument of type domain.

Equations

• Lean.Elab.WF.mkMutualArg numFuncs domain fidx arg = Lean.Elab.WF.mkMutualArg.go numFuncs fidx arg 0 domain

partial def Lean.Elab.WF.mkMutualArg.go (numFuncs : Nat) (fidx : Nat) (arg : Lean.Expr) (i : Nat) (type : Lean.Expr) : Lean.MetaM Lean.Expr

def Lean.Elab.WF.unpackMutualArg {m : Type → Type} [Monad m] [Lean.MonadError m] (numFuncs : Nat) (e : Lean.Expr) : m (Nat × Lean.Expr)

Unpacks a mutually packed argument, returning the argument and function index. Inverse of mkMutualArg. Cf. unpackUnaryArg and unpackArg, which does both

Equations

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

def Lean.Elab.WF.unpackArg {m : Type → Type} [Monad m] [Lean.MonadError m] (arities : Array Nat) (e : Lean.Expr) : m (Nat × Array Lean.Expr)

Given the packed argument of a (possibly) mutual and (possibly) nary call, return the function index that is called and the arguments individually.

We expect precisely the expressions produced by packMutual, with manifest PSum.inr, PSum.inl and PSigma.mk constructors, and thus take them apart rather than using projectinos.

Equations

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

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 α

Equations

• Lean.Elab.WF.withFixedPrefix fixedPrefix preDefs k = Lean.Elab.WF.withFixedPrefix.go preDefs k fixedPrefix #[] (Array.map (fun (x : Lean.Elab.PreDefinition) => x.value) preDefs)

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.

Equations

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