Create a unary application by packing the given arguments using PSigma.mk
Instances For
Convert the given pre-definitions into unary functions.
We "pack" the arguments using PSigma
.
Instances For
def
Lean.Elab.WF.packDomain.isAppOfPreDef?
(preDefs : Array Lean.Elab.PreDefinition)
(e : Lean.Expr)
:
Return some i
if e
is a preDefs[i]
application
Instances For
def
Lean.Elab.WF.packDomain.packApplications
(fixedPrefix : Nat)
(preDefs : Array Lean.Elab.PreDefinition)
(e : Lean.Expr)
(arities : Array Nat)
(preDefsNew : Array Lean.Elab.PreDefinition)
:
Instances For
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)
:
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)
: