Documentation

Lean.Elab.PreDefinition.Structural.Main

partial def Lean.Elab.Structural.withCommonTelescope.go {α : Type} (k : Array ExprArray ExprM α) (fvars vals : Array Expr) :
M α
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For