Documentation

Lean.Elab.BuiltinEvalCommand

Implementation of #eval command #

source
opaque Lean.Elab.Command.eval.pp :
Lean.Option Bool
source
opaque Lean.Elab.Command.eval.type :
Lean.Option Bool
source
opaque Lean.Elab.Command.eval.derive.repr :
Lean.Option Bool
source
unsafe def Lean.Elab.Command.elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax) (expectedType? : Option Expr) :
CommandElabM Unit
Equations
    Instances For
      source
      @[implemented_by Lean.Elab.Command.elabEvalCoreUnsafe]
      opaque Lean.Elab.Command.elabEvalCore (bang : Bool) (tk term : Syntax) (expectedType? : Option Expr) :
      CommandElabM Unit
      source
      def Lean.Elab.Command.elabEval :
      CommandElab
      Equations
        Instances For
          source
          def Lean.Elab.Command.elabEvalBang :
          CommandElab
          Equations
            Instances For
              source
              def Lean.Elab.Command.elabRunCmd :
              CommandElab
              Equations
                Instances For
                  source
                  def Lean.Elab.Command.elabRunElab :
                  CommandElab
                  Equations
                    Instances For
                      source
                      def Lean.Elab.Command.elabRunMeta :
                      CommandElab
                      Equations
                        Instances For