This is my code:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}

import Grisette

x :: SymInteger
x = "x"

y :: SymInteger
y = "y"

numbers :: [SymInteger]
numbers = [x, y]

n :: SymInteger
n = "n"

result :: UnionM [SymInteger]
result = symTake n numbers

main :: IO ()
main = do
    print $ result .== [1, 2]

I want to check whether result can be equal to [1, 2]. I can test if a simple list of symbolic integers can be equal to [1, 2]. For example, I can do this:

x :: SymInteger
x = "x"

y :: SymInteger
y = "y"

main :: IO ()
main = do
    print $ [x, y] .== [1, 2]

But I can’t find a way to do that with the result of symTake. Reading the code/docs in the code, it seems I’m not supposed to unbox the [SymInteger] out of the UnionM, but then I don’t know how do check for equality.