Documentation

Qq.ForLean.ReduceEval

source
def Lean.Meta.throwFailedToEval {α : Type} (e : Expr) :
MetaM α
Instances For
    source
    partial def Lean.Meta.evalList {α : Type} [ReduceEval α] (e : Expr) :
    MetaM (List α)
    source
    @[implicit_reducible]
    instance Lean.Meta.instReduceEvalList_qq {α : Type} [ReduceEval α] :
    ReduceEval (List α)
    source
    @[implicit_reducible]
    instance Lean.Meta.instReduceEvalFinOfNeZeroNat_qq {n : Nat} [NeZero n] :
    ReduceEval (Fin n)
    source
    @[implicit_reducible]
    instance Lean.Meta.instReduceEvalBitVec_qq {n : Nat} :
    ReduceEval (BitVec n)
    source
    @[implicit_reducible]
    instance Lean.Meta.instReduceEvalUInt64_qq :
    ReduceEval UInt64
    source
    @[implicit_reducible]
    instance Lean.Meta.instReduceEvalUSize_qq :
    ReduceEval USize
    source
    @[implicit_reducible]
    instance Lean.Meta.instReduceEvalBool_qq :
    ReduceEval Bool
    source
    @[implicit_reducible]
    instance Lean.Meta.instReduceEvalBinderInfo_qq :
    ReduceEval BinderInfo
    source
    @[implicit_reducible]
    instance Lean.Meta.instReduceEvalLiteral_qq :
    ReduceEval Literal
    source
    @[implicit_reducible]
    instance Lean.Meta.instReduceEvalMVarId_qq :
    ReduceEval MVarId
    source
    @[implicit_reducible]
    instance Lean.Meta.instReduceEvalLevelMVarId_qq :
    ReduceEval LevelMVarId
    source
    @[implicit_reducible]
    instance Lean.Meta.instReduceEvalFVarId_qq :
    ReduceEval FVarId