HepLean 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 : Lean.Syntax) (expectedType? : Option Lean.Expr) :
Lean.Elab.Command.CommandElabM Unit
Instances For
    source
    @[implemented_by Lean.Elab.Command.elabEvalCoreUnsafe]
    opaque Lean.Elab.Command.elabEvalCore (bang : Bool) (tk term : Lean.Syntax) (expectedType? : Option Lean.Expr) :
    Lean.Elab.Command.CommandElabM Unit
    source
    def Lean.Elab.Command.elabEval :
    Lean.Elab.Command.CommandElab
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Elab.Command.elabEvalBang :
      Lean.Elab.Command.CommandElab
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lean.Elab.Command.elabRunCmd :
        Lean.Elab.Command.CommandElab
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lean.Elab.Command.elabRunElab :
          Lean.Elab.Command.CommandElab
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lean.Elab.Command.elabRunMeta :
            Lean.Elab.Command.CommandElab
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For