This module is responsible for collecting the hypotheses out of the target that bv_decide was told to operate on.

• For regular MVarId-based targets it just collects everything from the local context.
• For grind's Goal-based targets it inspects the equivalence classes, in particular:
  • All members of True and False are collected as h : p and h : ¬ p respectively
  • For members of Bool, BitVec const and type analysis relevant eqcs it chooses a representative r and then collects the hypotheses h₁ : e₁ = r, ..., hₙ : eₙ = r. We try to choose an as-constant-as-possible representative to boost constant propagation and simplification in all of these hypotheses.

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.collectTargetHyps : PreProcessM Unit

Equations

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