Documentation

Qq.ForLean.ReduceEval

source
def Lean.Meta.throwFailedToEval {α : Type} (e : Lean.Expr) :
Lean.MetaM α
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    instance Lean.Meta.instReduceEvalList {α : Type} [Lean.Meta.ReduceEval α] :
    Lean.Meta.ReduceEval (List α)
    Equations
    • Lean.Meta.instReduceEvalList = { reduceEval := Lean.Meta.evalList }
    source
    instance Lean.Meta.instReduceEvalFinHAddNatInstHAddInstAddNatOfNat {n : Nat} :
    Lean.Meta.ReduceEval (Fin (n + 1))
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance Lean.Meta.instReduceEvalUInt64 :
    Lean.Meta.ReduceEval UInt64
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance Lean.Meta.instReduceEvalUSize :
    Lean.Meta.ReduceEval USize
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance Lean.Meta.instReduceEvalBool :
    Lean.Meta.ReduceEval Bool
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance Lean.Meta.instReduceEvalBinderInfo :
    Lean.Meta.ReduceEval Lean.BinderInfo
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance Lean.Meta.instReduceEvalLiteral :
    Lean.Meta.ReduceEval Lean.Literal
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance Lean.Meta.instReduceEvalMVarId :
    Lean.Meta.ReduceEval Lean.MVarId
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance Lean.Meta.instReduceEvalLevelMVarId :
    Lean.Meta.ReduceEval Lean.LevelMVarId
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance Lean.Meta.instReduceEvalFVarId :
    Lean.Meta.ReduceEval Lean.FVarId
    Equations
    • One or more equations did not get rendered due to their size.