Documentation

Qq.ForLean.ReduceEval

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

Equations

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

Instances For

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

MetaM (List α)

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

ReduceEval (List α)

Equations

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

instance Lean.Meta.instReduceEvalFinOfNeZeroNat_qq {n : Nat} [NeZero n] :

ReduceEval (Fin n)

Equations

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

instance Lean.Meta.instReduceEvalBitVec_qq {n : Nat} :

ReduceEval (BitVec n)

Equations

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

instance Lean.Meta.instReduceEvalUInt64_qq :

ReduceEval UInt64

Equations

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

instance Lean.Meta.instReduceEvalUSize_qq :

ReduceEval USize

Equations

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

instance Lean.Meta.instReduceEvalBool_qq :

ReduceEval Bool

Equations

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

instance Lean.Meta.instReduceEvalBinderInfo_qq :

ReduceEval BinderInfo

Equations

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

instance Lean.Meta.instReduceEvalLiteral_qq :

ReduceEval Literal

Equations

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

instance Lean.Meta.instReduceEvalMVarId_qq :

ReduceEval MVarId

Equations

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

instance Lean.Meta.instReduceEvalLevelMVarId_qq :

ReduceEval LevelMVarId

Equations

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

instance Lean.Meta.instReduceEvalFVarId_qq :

ReduceEval FVarId

Equations

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