Documentation

Lean.Meta.ReduceEval

Evaluation by reduction

source
class Lean.Meta.ReduceEval (α : Type) :
Type
Instances
    source
    def Lean.Meta.reduceEval {α : Type} [ReduceEval α] (e : Expr) :
    MetaM α
    Equations
      Instances For
        source
        instance Lean.Meta.instReduceEvalNat :
        ReduceEval Nat
        Equations
          source
          instance Lean.Meta.instReduceEvalOption {α : Type} [ReduceEval α] :
          ReduceEval (Option α)
          Equations
            source
            instance Lean.Meta.instReduceEvalString :
            ReduceEval String
            Equations
              source
              instance Lean.Meta.instReduceEvalName :
              ReduceEval Name
              Equations
                source
                instance Lean.Meta.instReduceEvalList {α : Type} [ReduceEval α] :
                ReduceEval (List α)
                Equations
                  source
                  instance Lean.Meta.instReduceEvalFinOfNeZeroNat {n : Nat} [NeZero n] :
                  ReduceEval (Fin n)
                  Equations
                    source
                    instance Lean.Meta.instReduceEvalBitVec {n : Nat} :
                    ReduceEval (BitVec n)
                    Equations
                      source
                      instance Lean.Meta.instReduceEvalBool :
                      ReduceEval Bool
                      Equations
                        source
                        instance Lean.Meta.instReduceEvalBinderInfo :
                        ReduceEval BinderInfo
                        Equations
                          source
                          instance Lean.Meta.instReduceEvalLiteral :
                          ReduceEval Literal
                          Equations
                            source
                            instance Lean.Meta.instReduceEvalMVarId :
                            ReduceEval MVarId
                            Equations
                              source
                              instance Lean.Meta.instReduceEvalLevelMVarId :
                              ReduceEval LevelMVarId
                              Equations
                                source
                                instance Lean.Meta.instReduceEvalFVarId :
                                ReduceEval FVarId
                                Equations