parameters: (name, sorts, ctx=None)
return_statement: return sum, [(sum.constructor(i), sum.accessor(i, 0)) for i in range(len(sorts))]
docstring: Create a named tagged union sort base on a set of underlying sorts
      Example:
          >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
docstring_summary: Create a named tagged union sort base on a set of underlying sorts
      Example:
          >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
docstring_tokens: Create a named tagged union sort base on a set of underlying sorts Example : >>> sum (( inject0 extract0 ) ( inject1 extract1 )) = DisjointSum ( + [ IntSort () StringSort () ] )
function: def DisjointSum(name, sorts, ctx=None):
      """Create a named tagged union sort base on a set of underlying sorts
      Example:
          >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
      """
      sum = Datatype(name, ctx)
      for i in range(len(sorts)):
          sum.declare("inject%d" % i, ("project%d" % i, sorts[i]))
      sum = sum.create()
      return sum, [(sum.constructor(i), sum.accessor(i, 0)) for i in range(len(sorts))]
function_tokens: def DisjointSum ( name , sorts , ctx = None ) : sum = Datatype ( name , ctx ) for i in range ( len ( sorts ) ) : sum . declare ( "inject%d" % i , ( "project%d" % i , sorts [ i ] ) ) sum = sum . create ( ) return sum , [ ( sum . constructor ( i ) , sum . accessor ( i , 0 ) ) for i in range ( len ( sorts ) ) ]