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 pand the auxiliary theoremseq_true_of_decide/eq_false_of_decide`.

Equations

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

def Lean.Meta.Simp.evalEqPropStep (e : Expr) (eq : Bool) (mkNeProof : SimpM Expr) : SimpM Step

Like evalPropStep, but specialized for @Eq.{u} α a b. When the values are equal, uses eq_true rfl which requires no kernel evaluation. When different, calls mkNeProof to build a proof of a ≠ b.

Equations

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

def Lean.Meta.Simp.evalNePropStep (e : Expr) (ne : Bool) (mkNeProof : SimpM Expr) : SimpM Step

Like evalPropStep, but specialized for @Ne.{u} α a b. When the values differ, calls mkNeProof to build a proof of a ≠ b. When equal, uses eq_false (not_not_intro rfl) which requires no kernel evaluation.

Equations

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