Documentation

Lean.Elab.Deriving.BEq

def Lean.Elab.Deriving.BEq.mkMatch (header : Header) (indVal : InductiveVal) (auxFunName : Name) :
Equations
    Instances For
      def Lean.Elab.Deriving.BEq.mkMatch.mkElseAlt (indVal : InductiveVal) :
      TermElabM (TSyntax `Lean.Parser.Term.matchAltExpr)
      Equations
        Instances For
          def Lean.Elab.Deriving.BEq.mkMatch.mkAlts (indVal : InductiveVal) (auxFunName : Name) :
          TermElabM (Array (TSyntax `Lean.Parser.Term.matchAlt))
          Equations
            Instances For