Documentation

Lean.Elab.Tactic.BVDecide.Frontend.BVTrace

This module contains the implementation of bv_decide?.

source
def Lean.Elab.Tactic.BVDecide.Frontend.BVTrace.getLratFileName :
TermElabM System.FilePath

Produce a file with the pattern: LeanFileName-DeclName-Line-Col.lrat

Equations
    Instances For
      source
      def Lean.Elab.Tactic.BVDecide.Frontend.BVTrace.evalBvTrace :
      Tactic
      Equations
        Instances For