source
def Lean.Meta.Grind.propagateProjEq (parent : 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.

Instances For