Documentation

Lean.Elab.Deriving.DecEq

source
def Lean.Elab.Deriving.DecEq.mkDecEqHeader (indVal : InductiveVal) :
TermElabM Header
Equations
    Instances For
      source
      def Lean.Elab.Deriving.DecEq.mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) :
      TermElabM Term
      Equations
        Instances For
          source
          def Lean.Elab.Deriving.DecEq.mkMatch.mkSameCtorRhs :
          List (Ident × Ident × Option Name × Bool) → TermElabM Term
          Equations
            Instances For
              source
              def Lean.Elab.Deriving.DecEq.mkMatch.mkAlts (ctx : Context) (indVal : InductiveVal) :
              TermElabM (Array (TSyntax `Lean.Parser.Term.matchAlt))
              Equations
                Instances For
                  source
                  def Lean.Elab.Deriving.DecEq.mkAuxFunction (ctx : Context) (auxFunName : Name) (indVal : InductiveVal) :
                  TermElabM (TSyntax `command)
                  Equations
                    Instances For
                      source
                      def Lean.Elab.Deriving.DecEq.mkAuxFunctions (ctx : Context) :
                      TermElabM (TSyntax `command)
                      Equations
                        Instances For
                          source
                          def Lean.Elab.Deriving.DecEq.mkDecEqCmds (indVal : InductiveVal) :
                          TermElabM (Array Syntax)
                          Equations
                            Instances For
                              source
                              def Lean.Elab.Deriving.DecEq.mkDecEq (declName : Name) :
                              Command.CommandElabM Bool
                              Equations
                                Instances For
                                  source
                                  def Lean.Elab.Deriving.DecEq.mkEnumOfNat (declName : Name) :
                                  MetaM Unit
                                  Equations
                                    Instances For
                                      source
                                      partial def Lean.Elab.Deriving.DecEq.mkEnumOfNat.mkDecTree (enumType : Expr) (ctors : Array Name) (n cond : Expr) (low high : Nat) :
                                      Expr
                                      source
                                      def Lean.Elab.Deriving.DecEq.mkEnumOfNatThm (declName : Name) :
                                      MetaM Unit
                                      Equations
                                        Instances For
                                          source
                                          def Lean.Elab.Deriving.DecEq.mkDecEqEnum (declName : Name) :
                                          Command.CommandElabM Unit
                                          Equations
                                            Instances For
                                              source
                                              def Lean.Elab.Deriving.DecEq.mkDecEqInstance (declName : Name) :
                                              Command.CommandElabM Bool
                                              Equations
                                                Instances For
                                                  source
                                                  def Lean.Elab.Deriving.DecEq.mkDecEqInstanceHandler (declNames : Array Name) :
                                                  Command.CommandElabM Bool
                                                  Equations
                                                    Instances For