def Lean.Meta.Simp.evalPropStep (p : Lean.Expr) (result : Bool) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Let result be the result of evaluating proposition p, return a .done step where the resulting expression is True(False) if result is true(false), and the proof is uses Decidable pand the auxiliary theoremseq_true_of_decide/eq_false_of_decide`.

Equations

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