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

• zeta
• zetaDelta
• beta
• ground term evaluation
• match of known ctor
• proj of ctor

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

Apply zeta, zetaDelta, beta, ground term evaluation, match of known ctor and proj of ctor.

Equations

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