Documentation

Lean.Meta.ReduceEval

Evaluation by reduction

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