def Lean.Meta.throwFailedToEval {α : Type} (e : Lean.Expr) : Lean.MetaM α

instance Lean.Meta.instReduceEvalList {α : Type} [Lean.Meta.ReduceEval α] : Lean.Meta.ReduceEval (List α)

instance Lean.Meta.instReduceEvalFinHAddNatInstHAddInstAddNatOfNat {n : Nat} : Lean.Meta.ReduceEval (Fin (n + 1))

instance Lean.Meta.instReduceEvalUInt64 : Lean.Meta.ReduceEval UInt64

instance Lean.Meta.instReduceEvalUSize : Lean.Meta.ReduceEval USize

instance Lean.Meta.instReduceEvalBool : Lean.Meta.ReduceEval Bool

instance Lean.Meta.instReduceEvalBinderInfo : Lean.Meta.ReduceEval Lean.BinderInfo

instance Lean.Meta.instReduceEvalLiteral : Lean.Meta.ReduceEval Lean.Literal

instance Lean.Meta.instReduceEvalMVarId : Lean.Meta.ReduceEval Lean.MVarId

instance Lean.Meta.instReduceEvalLevelMVarId : Lean.Meta.ReduceEval Lean.LevelMVarId

instance Lean.Meta.instReduceEvalFVarId : Lean.Meta.ReduceEval Lean.FVarId