Documentation
Qq
.
ForLean
.
ReduceEval
Search
return to top
source
Imports
Init
Lean
Imported by
Lean
.
Meta
.
throwFailedToEval
Lean
.
Meta
.
instReduceEvalList_qq
Lean
.
Meta
.
instReduceEvalFinOfNeZeroNat_qq
Lean
.
Meta
.
instReduceEvalBitVec_qq
Lean
.
Meta
.
instReduceEvalUInt64_qq
Lean
.
Meta
.
instReduceEvalUSize_qq
Lean
.
Meta
.
instReduceEvalBool_qq
Lean
.
Meta
.
instReduceEvalBinderInfo_qq
Lean
.
Meta
.
instReduceEvalLiteral_qq
Lean
.
Meta
.
instReduceEvalMVarId_qq
Lean
.
Meta
.
instReduceEvalLevelMVarId_qq
Lean
.
Meta
.
instReduceEvalFVarId_qq
source
def
Lean
.
Meta
.
throwFailedToEval
{
α
:
Type
}
(
e
:
Expr
)
:
MetaM
α
Equations
Instances For
source
instance
Lean
.
Meta
.
instReduceEvalList_qq
{
α
:
Type
}
[
ReduceEval
α
]
:
ReduceEval
(
List
α
)
Equations
source
instance
Lean
.
Meta
.
instReduceEvalFinOfNeZeroNat_qq
{
n
:
Nat
}
[
NeZero
n
]
:
ReduceEval
(
Fin
n
)
Equations
source
instance
Lean
.
Meta
.
instReduceEvalBitVec_qq
{
n
:
Nat
}
:
ReduceEval
(
BitVec
n
)
Equations
source
instance
Lean
.
Meta
.
instReduceEvalUInt64_qq
:
ReduceEval
UInt64
Equations
source
instance
Lean
.
Meta
.
instReduceEvalUSize_qq
:
ReduceEval
USize
Equations
source
instance
Lean
.
Meta
.
instReduceEvalBool_qq
:
ReduceEval
Bool
Equations
source
instance
Lean
.
Meta
.
instReduceEvalBinderInfo_qq
:
ReduceEval
BinderInfo
Equations
source
instance
Lean
.
Meta
.
instReduceEvalLiteral_qq
:
ReduceEval
Literal
Equations
source
instance
Lean
.
Meta
.
instReduceEvalMVarId_qq
:
ReduceEval
MVarId
Equations
source
instance
Lean
.
Meta
.
instReduceEvalLevelMVarId_qq
:
ReduceEval
LevelMVarId
Equations
source
instance
Lean
.
Meta
.
instReduceEvalFVarId_qq
:
ReduceEval
FVarId
Equations