Documentation

Lean.Meta.Tactic.BVDecide.Prover.Cegar.Lemmas

This module is responsible for draining the queue of new lemmas, pre-processing it and updating the BitVec abstraction accordingly.

source
inductive Lean.Meta.Tactic.BVDecide.ProcessHypResult :
Type
Instances For
    source
    def Lean.Meta.Tactic.BVDecide.Cegar.processNewHyps :
    CegarM ProcessHypResult
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For