Documentation

Lean.Elab.Deriving.Repr

Equations
    Instances For
      Equations
        Instances For
          def Lean.Elab.Deriving.Repr.mkBodyForInduct.mkAlts (header : Header) (indVal : InductiveVal) (auxFunName : Name) :
          TermElabM (Array (TSyntax `Lean.Parser.Term.matchAlt))
          Equations
            Instances For
              def Lean.Elab.Deriving.Repr.mkBody (header : Header) (indVal : InductiveVal) (auxFunName : Name) :
              Equations
                Instances For