Documentation

Lean.Meta.ReduceEval

Evaluation by reduction

class Lean.Meta.ReduceEval (α : Type) :

reduceEval : Expr → MetaM α

Instances

def Lean.Meta.reduceEval {α : Type} [ReduceEval α] (e : Expr) :

Equations

Lean.Meta.reduceEval e = Lean.Meta.withAtLeastTransparency Lean.Meta.TransparencyMode.default (Lean.Meta.ReduceEval.reduceEval e)

Instances For

instance Lean.Meta.instReduceEvalNat :

Equations

Lean.Meta.instReduceEvalNat = { reduceEval := fun (e : Lean.Expr) => Lean.Meta.instReduceEvalNat._private_1 e }

instance Lean.Meta.instReduceEvalOption {α : Type} [ReduceEval α] :

ReduceEval (Option α)

Equations

Lean.Meta.instReduceEvalOption = { reduceEval := fun (e : Lean.Expr) => Lean.Meta.instReduceEvalOption._private_1 e }

instance Lean.Meta.instReduceEvalString :

ReduceEval String

Equations

Lean.Meta.instReduceEvalString = { reduceEval := fun (e : Lean.Expr) => Lean.Meta.instReduceEvalString._private_1 e }

instance Lean.Meta.instReduceEvalName :

ReduceEval Name

Equations

Lean.Meta.instReduceEvalName = { reduceEval := Lean.Meta.instReduceEvalName._private_1 }

instance Lean.Meta.instReduceEvalList {α : Type} [ReduceEval α] :

ReduceEval (List α)

Equations

Lean.Meta.instReduceEvalList = { reduceEval := Lean.Meta.instReduceEvalList._private_1 }

instance Lean.Meta.instReduceEvalFinOfNeZeroNat {n : Nat} [NeZero n] :

ReduceEval (Fin n)

Equations

Lean.Meta.instReduceEvalFinOfNeZeroNat = { reduceEval := Lean.Meta.instReduceEvalFinOfNeZeroNat._private_1 }

instance Lean.Meta.instReduceEvalBitVec {n : Nat} :

ReduceEval (BitVec n)

Equations

Lean.Meta.instReduceEvalBitVec = { reduceEval := Lean.Meta.instReduceEvalBitVec._private_1 }

instance Lean.Meta.instReduceEvalBool :

ReduceEval Bool

Equations

Lean.Meta.instReduceEvalBool = { reduceEval := Lean.Meta.instReduceEvalBool._private_1 }

instance Lean.Meta.instReduceEvalBinderInfo :

ReduceEval BinderInfo

Equations

Lean.Meta.instReduceEvalBinderInfo = { reduceEval := Lean.Meta.instReduceEvalBinderInfo._private_1 }

instance Lean.Meta.instReduceEvalLiteral :

ReduceEval Literal

Equations

Lean.Meta.instReduceEvalLiteral = { reduceEval := Lean.Meta.instReduceEvalLiteral._private_1 }

instance Lean.Meta.instReduceEvalMVarId :

ReduceEval MVarId

Equations

Lean.Meta.instReduceEvalMVarId = { reduceEval := fun (e : Lean.Expr) => Lean.Meta.instReduceEvalMVarId._private_1 e }

instance Lean.Meta.instReduceEvalLevelMVarId :

ReduceEval LevelMVarId

Equations

Lean.Meta.instReduceEvalLevelMVarId = { reduceEval := fun (e : Lean.Expr) => Lean.Meta.instReduceEvalLevelMVarId._private_1 e }

instance Lean.Meta.instReduceEvalFVarId :

ReduceEval FVarId

Equations

Lean.Meta.instReduceEvalFVarId = { reduceEval := fun (e : Lean.Expr) => Lean.Meta.instReduceEvalFVarId._private_1 e }