Documentation

Qq.ForLean.ReduceEval

source
def Lean.Meta.throwFailedToEval {α : Type} (e : Expr) :
MetaM α
Equations
    Instances For
      source
      partial def Lean.Meta.evalList {α : Type} [ReduceEval α] (e : Expr) :
      MetaM (List α)
      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