def Lean.Meta.Grind.propagateForallPropUp (e : Expr) : GoalM Unit

Propagator for dependent forall terms forall (h : p), q[h] where p is a proposition.

def Lean.Meta.Grind.checkAnchorRefsEMatchTheoremProof (proof : Expr) : GrindM Bool

Given a proof of an EMatchTheorem, returns true, if there are no anchor references restricting the search, or there is an anchor references ref s.t. ref matches proof.

def Lean.Meta.Grind.propagateForallPropDown (e : Expr) : GoalM Unit

def Lean.Meta.Grind.propagateExistsDown : Propagator

def Lean.Meta.Grind.simpForall : Simp.Simproc

Applies the following rewriting rules:

• Grind.imp_true_eq
• Grind.imp_false_eq
• Grind.forall_imp_eq_or
• Grind.true_imp_eq
• Grind.false_imp_eq
• Grind.imp_self_eq
• forall_true
• forall_false
• Grind.forall_or_forall
• Grind.forall_forall_or
• Grind.forall_and

def Lean.Meta.Grind.simpExists : Simp.Simproc

Applies the following rewriting rules:

• Grind.exists_or
• Grind.exists_and_left
• Grind.exists_and_right
• Grind.exists_prop
• Grind.exists_const

def Lean.Meta.Grind.addForallSimproc (s : Simprocs) : CoreM Simprocs