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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.propagateForallPropUp e = pure ()

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.

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.propagateForallPropDown e = pure ()

def Lean.Meta.Grind.propagateExistsDown : Propagator

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.simpForall e = pure Lean.Meta.Simp.Step.continue

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

Equations

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

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

Equations

• Lean.Meta.Grind.addForallSimproc s = do let s ← s.add `Lean.Meta.Grind.simpForall true s.add `Lean.Meta.Grind.simpExists true