Documentation
Qq
.
ForLean
.
ReduceEval
Search
Google site search
Qq
.
ForLean
.
ReduceEval
source
Imports
Init
Lean
Imported by
Lean
.
Meta
.
throwFailedToEval
Lean
.
Meta
.
instReduceEvalList
Lean
.
Meta
.
instReduceEvalFinHAddNatInstHAddInstAddNatOfNat
Lean
.
Meta
.
instReduceEvalUInt64
Lean
.
Meta
.
instReduceEvalUSize
Lean
.
Meta
.
instReduceEvalBool
Lean
.
Meta
.
instReduceEvalBinderInfo
Lean
.
Meta
.
instReduceEvalLiteral
Lean
.
Meta
.
instReduceEvalMVarId
Lean
.
Meta
.
instReduceEvalLevelMVarId
Lean
.
Meta
.
instReduceEvalFVarId
source
def
Lean
.
Meta
.
throwFailedToEval
{α :
Type
}
(e :
Lean.Expr
)
:
Lean.MetaM
α
Instances For
source
instance
Lean
.
Meta
.
instReduceEvalList
{α :
Type
}
[
Lean.Meta.ReduceEval
α
]
:
Lean.Meta.ReduceEval
(
List
α
)
source
instance
Lean
.
Meta
.
instReduceEvalFinHAddNatInstHAddInstAddNatOfNat
{n :
Nat
}
:
Lean.Meta.ReduceEval
(
Fin
(
n
+
1
)
)
source
instance
Lean
.
Meta
.
instReduceEvalUInt64
:
Lean.Meta.ReduceEval
UInt64
source
instance
Lean
.
Meta
.
instReduceEvalUSize
:
Lean.Meta.ReduceEval
USize
source
instance
Lean
.
Meta
.
instReduceEvalBool
:
Lean.Meta.ReduceEval
Bool
source
instance
Lean
.
Meta
.
instReduceEvalBinderInfo
:
Lean.Meta.ReduceEval
Lean.BinderInfo
source
instance
Lean
.
Meta
.
instReduceEvalLiteral
:
Lean.Meta.ReduceEval
Lean.Literal
source
instance
Lean
.
Meta
.
instReduceEvalMVarId
:
Lean.Meta.ReduceEval
Lean.MVarId
source
instance
Lean
.
Meta
.
instReduceEvalLevelMVarId
:
Lean.Meta.ReduceEval
Lean.LevelMVarId
source
instance
Lean
.
Meta
.
instReduceEvalFVarId
:
Lean.Meta.ReduceEval
Lean.FVarId