Documentation

Lean.Elab.Tactic.Grind.BVDecide

Imports

Lean.Elab.Tactic.BVDecide
Lean.Elab.Tactic.Grind.Basic
Lean.Meta.Tactic.BVDecide.Main
Lean.Meta.Tactic.BVDecide.Normalize

Imported by

← Copula mathematical handbook

This module provides the implementation of the bv_decide family of tactics in sym => mode.