This module implements the reduction pass which applies various kinds of type theoretic reductions:

• zeta
• zetaDelta
• beta
• ground term evaluation

def Lean.Meta.Tactic.BVDecide.Normalize.reductionPass : Pass

Apply zeta, zetaDelta, beta, and ground term evaluation.

Equations

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