Documentation

Lean.Meta.ReduceEval

Evaluation by reduction

source
class Lean.Meta.ReduceEval (α : Type) :
Type
Instances
    source
    def Lean.Meta.reduceEval {α : Type} [ReduceEval α] (e : Expr) :
    MetaM α
    Equations
      Instances For
        source
        instance Lean.Meta.instReduceEvalNat :
        ReduceEval Nat
        Equations
          source
          instance Lean.Meta.instReduceEvalOption {α : Type} [ReduceEval α] :
          ReduceEval (Option α)
          Equations
            source
            instance Lean.Meta.instReduceEvalString :
            ReduceEval String
            Equations
              source
              instance Lean.Meta.instReduceEvalName :
              ReduceEval Name
              Equations