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
Instances For
    source
    def Lean.Elab.ConfigEval.elabEnsureEvalExprInstance :
    Command.CommandElab
    Instances For
      source
      def Lean.Elab.ConfigEval.expandEnsureEvalTermExprInstance :
      Macro
      Instances For
        source
        def Lean.Elab.ConfigEval.elabDeriveEvalExprUsingMeta :
        Command.CommandElab
        Instances For
          source
          def Lean.Elab.ConfigEval.mkEvalConfigItemView (entries? : Option (TSyntax `Lean.Elab.ConfigEval.configEntries)) :
          Command.CommandElabM EvalConfigItemView
          Instances For
            source
            def Lean.Elab.ConfigEval.elabDefEvalConfigItemCmd :
            Command.CommandElab
            Instances For
              source
              def Lean.Elab.ConfigEval.elabDeclareCoreConfigElab :
              Macro
              Instances For
                source
                def Lean.Elab.ConfigEval.elabDeclareTermConfigElab :
                Macro
                Instances For
                  source
                  def Lean.Elab.ConfigEval.elabDeclareTacticConfig :
                  Macro
                  Instances For
                    source
                    def Lean.Elab.ConfigEval.elabDeclareCommandConfig :
                    Macro
                    Instances For