Method EnumSort

src/api/java/EnumSort.java:95–101

(Context ctx, Symbol name, Symbol[] enumNames)

    }

    EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
    {
        super(ctx, Native.mkEnumerationSort(ctx.nCtx(),
                name.getNativeObject(), enumNames.length,
                Symbol.arrayToNative(enumNames),
                new long[enumNames.length], new long[enumNames.length]));
    }
};