Documentation

Lean.Meta.Tactic.BVDecide.Normalize.Reduction

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

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

Instances For