Documentation

Lean.Elab.ConfigEval.Builtins

Builtin elaborators and macros for ConfigEval commands #

The elaborators are builtins to avoid bootstrapping issues in core Lean.

source
def Lean.Elab.ConfigEval.elabEnsureEvalTermInstance :
Command.CommandElab
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Elab.ConfigEval.elabEnsureEvalExprInstance :
    Command.CommandElab
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Elab.ConfigEval.expandEnsureEvalTermExprInstance :
      Macro
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lean.Elab.ConfigEval.elabDeriveEvalExprUsingMeta :
        Command.CommandElab
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lean.Elab.ConfigEval.mkEvalConfigItemView (entries? : Option (TSyntax `Lean.Elab.ConfigEval.configEntries)) :
          Command.CommandElabM EvalConfigItemView
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lean.Elab.ConfigEval.elabDefEvalConfigItemCmd :
            Command.CommandElab
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Lean.Elab.ConfigEval.elabDeclareCoreConfigElab :
              Macro
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Lean.Elab.ConfigEval.elabDeclareTermConfigElab :
                Macro
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Lean.Elab.ConfigEval.elabDeclareTacticConfig :
                  Macro
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Lean.Elab.ConfigEval.elabDeclareCommandConfig :
                    Macro
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For