Documentation

Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.ReifiedBVLogical

Provides the logic for reifying BitVec problems with boolean substructure.

source
def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkRefl (expr : Expr) :
Expr
Instances For
    source
    def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkTrans (x y z hxy hyz : Expr) :
    Expr
    Instances For
      source
      def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkEvalExpr (expr : Expr) :
      M Expr
      Instances For
        source
        def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.ofPred (bvPred : ReifiedBVPred) :
        M ReifiedBVLogical

        Construct a ReifiedBVLogical from ReifiedBVPred by wrapping it as an atom.

        Instances For
          source
          def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.boolAtom (t : Expr) :
          M (Option ReifiedBVLogical)

          Construct an uninterpreted Bool atom from t.

          Instances For
            source
            def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkBoolConst (val : Bool) :
            M ReifiedBVLogical

            Build a reified version of the constant val.

            Instances For
              source
              def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Std.Tactic.BVDecide.Gate) (origExpr : Expr) :
              M ReifiedBVLogical

              Construct the reified version of applying the gate in gate to lhs and rhs. This function assumes that lhsExpr and rhsExpr are the corresponding expressions to lhs and rhs.

              Instances For
                source
                def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkNot (sub : ReifiedBVLogical) (subExpr origExpr : Expr) :
                M ReifiedBVLogical

                Construct the reified version of Bool.not subExpr. This function assumes that subExpr is the expression corresponding to sub.

                Instances For
                  source
                  def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr origExpr : Expr) :
                  M ReifiedBVLogical

                  Construct the reified version of if discrExpr then lhsExpr else rhsExpr. This function assumes that discrExpr, lhsExprandrhsExprare the corresponding expressions to `discr, lhsandrhs`.

                  Instances For