Documentation

Lean.Meta.Tactic.BVDecide.Reflect.Reify

Reifies BitVec problems with boolean substructure.

source
def Lean.Meta.Tactic.BVDecide.isValidBitVecAtom (e : Expr) :
ReifyM (Option Nat)
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Meta.Tactic.BVDecide.isValidBoolAtom (e : Expr) :
    ReifyM Bool
    Equations
    Instances For
      source
      partial def Lean.Meta.Tactic.BVDecide.ReifiedBVExpr.bitVecAtom (e : Expr) (synthetic : Bool) :
      LemmaM (Option ReifiedBVExpr)

      Construct an uninterpreted BitVec atom from x, potentially synthetic.

      source
      partial def Lean.Meta.Tactic.BVDecide.ReifiedBVPred.boolAtom (e : Expr) :
      LemmaM (Option ReifiedBVPred)

      Construct an uninterpreted Bool atom from origExpr.

      source
      partial def Lean.Meta.Tactic.BVDecide.ReifiedBVLogical.boolAtom (t : Expr) :
      LemmaM (Option ReifiedBVLogical)

      Construct an uninterpreted Bool atom from t.

      source
      partial def Lean.Meta.Tactic.BVDecide.ReifiedBVExpr.of (origExpr : Expr) :
      LemmaM (Option ReifiedBVExpr)

      Reify an Expr that's a constant-width BitVec. Unless this function is called on something that is not a constant-width BitVec it is always going to return some.

      source
      partial def Lean.Meta.Tactic.BVDecide.ReifiedBVPred.of (origExpr : Expr) :
      LemmaM (Option ReifiedBVPred)

      Reify an Expr that is a predicate about BitVec. Unless this function is called on something that is not a Bool it is always going to return some.

      source
      partial def Lean.Meta.Tactic.BVDecide.ReifiedBVLogical.of (origExpr : Expr) :
      LemmaM (Option ReifiedBVLogical)

      Reify an Expr that is a boolean expression containing predicates about BitVec as atoms. Unless this function is called on something that is not a Bool it is always going to return some.