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

Equations

• Lean.Meta.throwFailedToEval e = Lean.throwError (Lean.toMessageData "reduceEval: failed to evaluate argument" ++ Lean.toMessageData (Lean.indentExpr e) ++ Lean.toMessageData "")

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

Equations

• Lean.Meta.instReduceEvalList_qq = { reduceEval := Lean.Meta.evalList✝ }

instance Lean.Meta.instReduceEvalFinOfNeZeroNat_qq {n : Nat} [NeZero n] : Lean.Meta.ReduceEval (Fin n)

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Meta.instReduceEvalBitVec_qq {n : Nat} : Lean.Meta.ReduceEval (BitVec n)

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Meta.instReduceEvalUInt64_qq : Lean.Meta.ReduceEval UInt64

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Meta.instReduceEvalUSize_qq : Lean.Meta.ReduceEval USize

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Meta.instReduceEvalBool_qq : Lean.Meta.ReduceEval Bool

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Meta.instReduceEvalBinderInfo_qq : Lean.Meta.ReduceEval Lean.BinderInfo

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Meta.instReduceEvalLiteral_qq : Lean.Meta.ReduceEval Lean.Literal

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Meta.instReduceEvalMVarId_qq : Lean.Meta.ReduceEval Lean.MVarId

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Meta.instReduceEvalLevelMVarId_qq : Lean.Meta.ReduceEval Lean.LevelMVarId

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Meta.instReduceEvalFVarId_qq : Lean.Meta.ReduceEval Lean.FVarId

Equations

• One or more equations did not get rendered due to their size.