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 : Lean.Expr) :
Lean.Expr
Instances For
    source
    def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkTrans (x y z hxy hyz : Lean.Expr) :
    Lean.Expr
    Equations
    Instances For
      source
      def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkEvalExpr (expr : Lean.Expr) :
      Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr
      Instances For
        source
        def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.ofPred (bvPred : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred) :
        Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical

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

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

          Construct an uninterrpeted Bool atom from t.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkBoolConst (val : Bool) :
            Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical

            Build a reified version of the constant val.

            Instances For
              source
              def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkGate (lhs rhs : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical) (lhsExpr rhsExpr : Lean.Expr) (gate : Std.Tactic.BVDecide.Gate) :
              Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Elab.Tactic.BVDecide.Frontend.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.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkGate.congrThmOfGate (gate : Std.Tactic.BVDecide.Gate) :
                Lean.Name
                Instances For
                  source
                  def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkNot (sub : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical) (subExpr : Lean.Expr) :
                  Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkIte (discr lhs rhs : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Lean.Expr) :
                    Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Elab.Tactic.BVDecide.Frontend.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