Documentation

Lean.Elab.PreDefinition.Structural.Main

source
def Lean.Elab.Structural.withCommonTelescope {α : Type} (preDefs : Array Lean.Elab.PreDefinition) (k : Array Lean.Expr → Array Lean.Expr → Lean.Elab.Structural.M α) :
Lean.Elab.Structural.M α
Equations
Instances For
    source
    partial def Lean.Elab.Structural.withCommonTelescope.go {α : Type} (k : Array Lean.Expr → Array Lean.Expr → Lean.Elab.Structural.M α) (fvars : Array Lean.Expr) (vals : Array Lean.Expr) :
    Lean.Elab.Structural.M α
    source
    def Lean.Elab.Structural.getMutualFixedPrefix (preDefs : Array Lean.Elab.PreDefinition) :
    Lean.Elab.Structural.M Nat
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Elab.Structural.reportTermArg (preDef : Lean.Elab.PreDefinition) (recArgPos : Nat) :
      Lean.MetaM Unit
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lean.Elab.Structural.structuralRecursion (preDefs : Array Lean.Elab.PreDefinition) (termArg?s : Array (Option Lean.Elab.TerminationArgument)) :
        Lean.Elab.TermElabM Unit
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For