Documentation

Lean.Meta.ReduceEval

Evaluation by reduction

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

Type

reduceEval : Lean.Expr → Lean.MetaM α

Instances

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

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} [inst : 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 Lean.Name

Equations

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