Documentation

Lean.Elab.PreDefinition.WF.PackDomain

source
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

Instances For
    source
    partial def Lean.Elab.WF.mkUnaryArg.go (args : Array Lean.Expr) (i : Nat) (type : Lean.Expr) :
    Lean.MetaM Lean.Expr
    source
    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.

    Instances For
      source
      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

      Instances For
        source
        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
        Instances For
          source
          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
          source
          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