source
def Lean.Meta.Simp.evalPropStep (p : Expr) (result : Bool) :
SimpM 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 p`and the auxiliary theorems`eq_true_of_decide`/`eq_false_of_decide`.

Equations

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

Instances For