Documentation

Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVLogical

Provides the logic for reifying BitVec problems with boolean substructure.

source
def Lean.Meta.Tactic.BVDecide.ReifiedBVLogical.mkRefl (expr : Expr) :
Expr
Equations
Instances For
    source
    def Lean.Meta.Tactic.BVDecide.ReifiedBVLogical.mkTrans (x y z hxy hyz : Expr) :
    Expr
    Equations
    Instances For
      source
      def Lean.Meta.Tactic.BVDecide.ReifiedBVLogical.mkEvalExpr (expr : Expr) :
      ReifyM Expr
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lean.Meta.Tactic.BVDecide.ReifiedBVLogical.mkBoolConst (val : Bool) :
        ReifyM ReifiedBVLogical

        Build a reified version of the constant val.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lean.Meta.Tactic.BVDecide.ReifiedBVLogical.mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Std.Tactic.BVDecide.Gate) (origExpr : Expr) :
          ReifyM 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.Meta.Tactic.BVDecide.ReifiedBVLogical.mkNot (sub : ReifiedBVLogical) (subExpr origExpr : Expr) :
            ReifyM 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.Meta.Tactic.BVDecide.ReifiedBVLogical.mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr origExpr : Expr) :
              ReifyM ReifiedBVLogical

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Lean.Meta.Tactic.BVDecide.ReifiedBVLogical.ofPred (bvPred : ReifiedBVPred) :
                ReifyM ReifiedBVLogical

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

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