source
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 ()

Instances For

source
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 ()

Instances For

source
def Lean.Meta.Grind.propagateExistsDown :
Propagator
Equations

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

Instances For

source
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

Instances For

source
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.

Instances For

source
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

Instances For