Evaluation by reduction

class Lean.Meta.ReduceEval (α : Type) : Type

• reduceEval : Expr → MetaM α

def Lean.Meta.reduceEval {α : Type} [ReduceEval α] (e : Expr) : MetaM α

Equations

• Lean.Meta.reduceEval e = Lean.Meta.withAtLeastTransparency Lean.Meta.TransparencyMode.default (Lean.Meta.ReduceEval.reduceEval e)

instance Lean.Meta.instReduceEvalNat : ReduceEval Nat

Equations

• Lean.Meta.instReduceEvalNat = { reduceEval := fun (e : Lean.Expr) => Lean.Meta.instReduceEvalNat._private_1 e }

instance Lean.Meta.instReduceEvalOption {α : Type} [ReduceEval α] : ReduceEval (Option α)

Equations

• Lean.Meta.instReduceEvalOption = { reduceEval := fun (e : Lean.Expr) => Lean.Meta.instReduceEvalOption._private_1 e }

instance Lean.Meta.instReduceEvalString : ReduceEval String

Equations

• Lean.Meta.instReduceEvalString = { reduceEval := fun (e : Lean.Expr) => Lean.Meta.instReduceEvalString._private_1 e }

instance Lean.Meta.instReduceEvalName : ReduceEval Name

Equations

• Lean.Meta.instReduceEvalName = { reduceEval := Lean.Meta.instReduceEvalName._private_1 }