Evaluation by reduction

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

• reduceEval : Lean.Expr → Lean.MetaM α

Instances

• Lean.Meta.instReduceEvalBinderInfo
• Lean.Meta.instReduceEvalBool
• Lean.Meta.instReduceEvalFVarId
• Lean.Meta.instReduceEvalFinHAddNatInstHAddInstAddNatOfNat
• Lean.Meta.instReduceEvalLevelMVarId
• Lean.Meta.instReduceEvalList
• Lean.Meta.instReduceEvalLiteral
• Lean.Meta.instReduceEvalMVarId
• Lean.Meta.instReduceEvalName
• Lean.Meta.instReduceEvalNat
• Lean.Meta.instReduceEvalOption
• Lean.Meta.instReduceEvalString
• Lean.Meta.instReduceEvalUInt64
• Lean.Meta.instReduceEvalUSize

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

Equations

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

instance Lean.Meta.instReduceEvalNat : Lean.Meta.ReduceEval Nat

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Meta.instReduceEvalString : Lean.Meta.ReduceEval String

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Meta.instReduceEvalName : Lean.Meta.ReduceEval Lake.Name

Equations

• Lean.Meta.instReduceEvalName = { reduceEval := Lean.Meta.evalName }