code: def Concat(*args: Union[BitVec, List[BitVec]]) -> BitVec:
      
      # The following statement is used if a list is provided as an argument to concat
      if len(args) == 1 and isinstance(args[0], list):
          bvs = args[0]  # type: List[BitVec]
      else:
          bvs = cast(List[BitVec], args)
  
      nraw = z3.Concat([a.raw for a in bvs])
      annotations = []  # type: Annotations
      bitvecfunc = False
      for bv in bvs:
          annotations += bv.annotations
          if isinstance(bv, BitVecFunc):
              bitvecfunc = True
  
      if bitvecfunc:
          # Is there a better value to set func_name and input to in this case?
          return BitVecFunc(
              raw=nraw, func_name=None, input_=None, annotations=annotations
          )
  
      return BitVec(nraw, annotations)
docs: Create a concatenation expression.
  
      :param args:
      :return: