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.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

• Lean.Elab.WF.packDomain.isAppOfPreDef? preDefs e = let f := Lean.Expr.getAppFn e; do guard (Lean.Expr.isConst f = true) Array.findIdx? preDefs fun x => x.declName == Lean.Expr.constName! f

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