Lean.Meta.ReduceEval

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

Type

Instances

Equations

Equations

Lean.Meta.instReduceEvalNat = { reduceEval := fun e => do let e ← Lean.Meta.whnf e let discr ← Lean.Meta.evalNat e match discr with | some n => pure n | x => Lean.Meta.throwFailedToEval e }

Equations

Lean.Meta.instReduceEvalOption = { reduceEval := fun e => do let e ← Lean.Meta.whnf e let discr ← pure (Lean.Expr.getAppFn e) match discr with | Lean.Expr.const c x x_1 => let nargs := Lean.Expr.getAppNumArgs e; if (c == `Option.none && nargs == 0) = true then pure none else if (c == `Option.some && nargs == 1) = true then some <$> Lean.Meta.reduceEval (Lean.Expr.appArg! e) else Lean.Meta.throwFailedToEval e | x => Lean.Meta.throwFailedToEval e }

Equations

Equations