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

If parent is a projection-application proj_i c, check whether the root of the equivalence class containing c is a constructor-application ctor ... a_i .... If so, internalize the term proj_i (ctor ... a_i ...) and add the equality proj_i (ctor ... a_i ...) = a_i.

Equations

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

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

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