def Lean.Elab.WF.mkUnaryArg (type : Lean.Expr) (args : Array Lean.Expr) : Lean.MetaM Lean.Expr

Create a unary application by packing the given arguments using PSigma.mk

Equations

• Lean.Elab.WF.mkUnaryArg type args = Lean.Elab.WF.mkUnaryArg.go args 0 type

partial def Lean.Elab.WF.mkUnaryArg.go (args : Array Lean.Expr) (i : Nat) (type : Lean.Expr) : Lean.MetaM Lean.Expr

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

Unpacks a unary packed argument created with mkUnaryArg.

Equations

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

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

Convert the given pre-definitions into unary functions. We "pack" the arguments using PSigma.

Equations

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

def Lean.Elab.WF.packDomain.isAppOfPreDef? (preDefs : Array Lean.Elab.PreDefinition) (e : Lean.Expr) : Option Nat

Return some i if e is a preDefs[i] application

Equations

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

def Lean.Elab.WF.packDomain.packApplications (fixedPrefix : Nat) (preDefs : Array Lean.Elab.PreDefinition) (e : Lean.Expr) (arities : Array Nat) (preDefsNew : Array Lean.Elab.PreDefinition) : Lean.MetaM Lean.Expr

Equations

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

partial def Lean.Elab.WF.packDomain.packApplications.visit (preDefs : Array Lean.Elab.PreDefinition) (arities : Array Nat) (pack : Lean.Expr → Nat → Lean.MetaM Lean.Expr) (e : Lean.Expr) : Lean.MonadCacheT Lean.ExprStructEq Lean.Expr Lean.MetaM Lean.Expr

partial def Lean.Elab.WF.packDomain.packApplications.visitApp (preDefs : Array Lean.Elab.PreDefinition) (arities : Array Nat) (pack : Lean.Expr → Nat → Lean.MetaM Lean.Expr) (e : Lean.Expr) : Lean.MonadCacheT Lean.ExprStructEq Lean.Expr Lean.MetaM Lean.Expr