Documentation

Lean.Elab.Deriving.Basic

source
def Lean.Elab.Term.processDefDeriving (classStx : Syntax) (decl : Expr) :
TermElabM Unit

Delta deriving handler. Creates an instance of class classStx for decl. The elaborated class expression may be underapplied (e.g. Decidable instead of Decidable _), and may be decl. If unfolding decl results in an underapplied lambda, then this enters the body of the lambda. We prevent classStx from referring to these local variables; instead it's expected that one uses section variables.

This function can handle being run from within a nontrivial local context, and it uses mkValueTypeClosure to construct the final instance.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Elab.DerivingHandler :
    Type
    Equations
    Instances For
      source
      opaque Lean.Elab.derivingHandlersRef :
      IO.Ref (NameMap (List DerivingHandler))
      source
      def Lean.Elab.registerDerivingHandler (className : Name) (handler : DerivingHandler) :
      IO Unit

      Registers a deriving handler for a class. This function should be called in an initialize block.

      A DerivingHandler is called on the fully qualified names of all types it is running for. For example, deriving instance Foo for Bar, Baz invokes fooHandler #[`Bar, `Baz].

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lean.Elab.applyDerivingHandlers (className : Name) (typeNames : Array Name) :
        Command.CommandElabM Unit
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lean.Elab.elabDeriving :
          Command.CommandElab
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            structure Lean.Elab.DerivingClassView :
            Type
            Instances For
              source
              def Lean.Elab.getOptDerivingClasses (optDeriving : Syntax) :
              CoreM (Array DerivingClassView)
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Lean.Elab.DerivingClassView.applyHandlers (view : DerivingClassView) (declNames : Array Name) :
                Command.CommandElabM Unit
                Equations
                Instances For