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 α
    Instances For
      source
      @[implicit_reducible]
      instance Lean.Meta.instReduceEvalNat :
      ReduceEval Nat
      source
      @[implicit_reducible]
      instance Lean.Meta.instReduceEvalOption {α : Type} [ReduceEval α] :
      ReduceEval (Option α)
      source
      @[implicit_reducible]
      instance Lean.Meta.instReduceEvalString :
      ReduceEval String
      source
      @[implicit_reducible]
      instance Lean.Meta.instReduceEvalName :
      ReduceEval Name
      source
      @[implicit_reducible]
      instance Lean.Meta.instReduceEvalList {α : Type} [ReduceEval α] :
      ReduceEval (List α)
      source
      @[implicit_reducible]
      instance Lean.Meta.instReduceEvalFinOfNeZeroNat {n : Nat} [NeZero n] :
      ReduceEval (Fin n)
      source
      @[implicit_reducible]
      instance Lean.Meta.instReduceEvalBitVec {n : Nat} :
      ReduceEval (BitVec n)
      source
      @[implicit_reducible]
      instance Lean.Meta.instReduceEvalBool :
      ReduceEval Bool
      source
      @[implicit_reducible]
      instance Lean.Meta.instReduceEvalBinderInfo :
      ReduceEval BinderInfo
      source
      @[implicit_reducible]
      instance Lean.Meta.instReduceEvalLiteral :
      ReduceEval Literal
      source
      @[implicit_reducible]
      instance Lean.Meta.instReduceEvalMVarId :
      ReduceEval MVarId
      source
      @[implicit_reducible]
      instance Lean.Meta.instReduceEvalLevelMVarId :
      ReduceEval LevelMVarId
      source
      @[implicit_reducible]
      instance Lean.Meta.instReduceEvalFVarId :
      ReduceEval FVarId