Documentation

Lean.Elab.PreDefinition.WF.Eqns

Instances For
    def Lean.Elab.WF.registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedParamPerms : FixedParamPerms) (argsPacker : Meta.ArgsPacker) :
    Equations
      Instances For
        Equations
          Instances For