Documentation

Lean.Elab.PreDefinition.Structural.Main

Equations
    Instances For
      partial def Lean.Elab.Structural.withCommonTelescope.go {α : Type} (k : Array ExprArray ExprM α) (fvars vals : Array Expr) :
      M α
      Equations
        Instances For